NUSMV has both a batch and an interactive mode. The batch mode offers a built-in method for dealing with the system in which computations are activated according to a fixed predefined algorithm. The batch mode provides an interaction with the system that is essentially the same provided by CMU SMV.
In the interactive mode computation steps are activated by commands executed by a command line interpreter, thus allowing for the modification of the predefined model checking algorithm. The definition of the interactive shell required the decomposition of the model checking algorithm into small basic computation steps (e.g., parsing, model construction, reachability analysis, model checking). In the current version of the system, each of them corresponds to a command that implements a different functionality.
The three modes of interaction with the NUSMV system, namely, the interactive shell, the batch mode and the graphical user interface are described below.
>