In general it is very useful to represent systems using enumerated types. As
symbolic algorithms work on boolean variables, there is the need to encode
propositions about non-boolean variables
in the space of boolean variables. There are different ways to perform this
task. At the moment NUSMV provides the encoding used in CMU SMV, which
represents a finite range variable with a sequence of boolean
variables. Consider a state variable
st that can assume the values
propositions on the possible values of
st can be encoded with
three boolean variables
as shown in Table 2.
Notice that the value assigned to the boolean variable st2, in the case of , is indifferent, and it can be either or 1.7 The boolean variables used to encode a scalar variable are grouped together, and are considered as a single block of variables in the BDD package. Other encoding policies can be more appropriate for variables of different kind. For example, word level encodings are useful for the analysis of data paths . Moreover, the constraint of grouping the boolean variables together can be relaxed. Some of these policies will be codified in further releases of NUSMV.