next up previous
Next: Counterexamples Generation. Up: Standard Functionalities Previous: Fair CTL model checking.

Check for Transition Relation Totality.

In NUSMV it is possible to check the totality of the transition relation. The check is performed by means of basic model checking operations:

$T(\cdot,\cdot)$ is total if and only if $\overline{\mathbf{EX}(\top)} = \bot$
This functionality is very useful if the keywords TRANS or INVAR9 are used to specify the transition relation. In these cases it is in fact possible to introduce deadlock states.

NuSMV <>