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 INVAR⁹ are used to specify the transition relation. In these cases it is in fact possible to introduce deadlock states.