Nondeterministic assignments

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.