nusmv

Assign random value to variables in NuSMV

I have the following code in NuSMV.

MODULE main
VAR
   x : 0..5

So x is a variable which can take integer values 0,1,2,3,4,5. Next, I initialize it and lay down its transition rules.

ASSIGN
    init(x):=1;
    next(x) := case
         y=1 & z=23: 4;
         TRUE: 0..5;
    esac;

What above should say is that x is initially 1. Then if y=1 and z=23, x becomes 4 otherwise x can assume any random values from its domain. This 'otherwise' part of the logic is what I am doubtful. Have I coded this correctly? y and z are variables whose codes are not shown here. Assume something for y and z.

Or should I have written:

TRUE: {0,1,2,3,4,5};

Because I definitely know the above to be correct from page 4 of this document.

But this is infeasible for a very large domain. Suppose x could take any value from 0 to 293.

Solution

  • Yes, it is correct.

    The integer set {0, 1, 2, 3, 4, 5} can also be written as 0 .. 5, as per the following documentation:

    2.1.6 Set Types

    set types are used to identify expressions representing a set of values. There are four set types: boolean set, integer set, symbolic set, integers-and-symbolic set. The set types can be used in a very limited number of ways. In particular, a variable cannot be of a set type. Only range constant and union operator can be used to create an expression of a set type, and only in, case, (• ? • : •) and assignment expressions can have imediate operands of a set type.

    Every set type has a counterpart among other types. In particular,

    • the counterpart of a boolean set type is boolean,

    • the counterpart of a integer set type is integer,

    • the counterpart of a symbolic set type is symbolic enum,

    • the counterpart of a integers-and-symbolic set type is integers-and-symbolic enum.

    Some types such as unsigned word[•] and signed word[•] do not have a set type counterpart.

    and

    Range Constant

    A range constant specifies a set of consecutive integer numbers. For example, a constant -1..5 indicates the set of numbers -1, 0, 1, 2, 3, 4 and 5. Other examples of range constant can be 1..10, -10..-10, 1..300. The syntactic rule of the range constant is the following:

    range_constant
    :: integer_number .. integer_number

    with an additional constraint that the first integer number must be less than or equal to the second integer number. The type of a range constant is integer set.