Especially in the early stages of a design, a designer may not want to completely specify the value of a given signal. Incomplete specification may represent either a design choice yet to be made, incomplete information about the environment of a system, or a deliberate abstraction made to simplify the verification of a system. For this purpose, SMV provides nondeterministic choice. A nondeterministic choice is represented by a set of values. If we make the assignment
signal := {a,b,c,d};
then the value of signal is
chosen arbitrarily from the set {a,b,c,d}. As another example, suppose
that in our previous state machine, we don't want to specify how
many cycles will be spent in state ``cyc1''. In this case, we could
write:
next(state) :=
switch(state){
idle: start ? cyc1 : idle;
cyc1: {cyc1,cyc2};
cyc2: idle;
};
Note that in case state = cyc1, the value of the switch expression is the set {cyc1,cyc2}. This means that the next value of ``state'' may be either ``cyc1'' or ``cyc2''. In general, the mathematical meaning of the assignment
x := y;where y is a set of values, is that x is included in the set y. Ordinary values are treated as sets of size one. Thus, properly speaking, an SMV program is a simultaneous set of inclusions, rather than equations.