Encoding.

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 $\mathtt{\{a, b, c, d, e\}}$. The propositions on the possible values of st can be encoded with three boolean variables st₀, st₁ and st₂, as shown in Table 2.

 

Table 2: The encoding of a variable ``st'' that can assume the values ``a'', ``b'', ``c'', ``d'' and ``e''.

Symbolic Value	Boolean Encoding
st = a	$\mathtt{st_0 = 0 \wedge st_1 = 0 \wedge st_2 = 0}$
st = b	$\mathtt{st_0} = 1 \wedge \mathtt{st_1} = 0$
st = c	$\mathtt{st_0} = 0 \wedge \mathtt{st_1} = 1$
st = d	$\mathtt{st_0} = 1 \wedge \mathtt{st_1} = 1$
st = e	$\mathtt{st_0} = 0 \wedge \mathtt{st_1} = 0 \wedge \mathtt{st_2} = 1$

 

Notice that the value assigned to the boolean variable st₂, in the case of $\mathtt{st} \in \{\mathtt{b}, \mathtt{c}, \mathtt{d}\}$, is indifferent, and it can be either or 1.⁷ 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 [25]. Moreover, the constraint of grouping the boolean variables together can be relaxed. Some of these policies will be codified in further releases of NUSMV.