Next: Counterexamples Generation.
Up: Standard Functionalities
Previous: Fair CTL model checking.
In NUSMV it is possible to check the totality of the transition
relation. The check is performed by means of basic model checking
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.
is total if and only if