This approach is not very direct, and can be quite inefficient. If the set of reachable states has been previously computed, then an invariant can be simply checked by performing a test of set inclusion between the states represented by and the set of reachable states:

NUSMV offers the possibility of checking invariants using either this or the standard model checking technique. These functionalities are the same as in CMU SMV. Moreover NUSMV, w.r.t. CMU SMV, has a specialized routine for checking invariants on the fly. This is performed by verifying at each step

where is the set of states reachable in

NuSMV <>