Go to the first, previous, next, last section, table of contents.
NuSMV interactively
The main interaction mode of NuSMV is through an interactive
shell. In this mode NuSMV enters a read-eval-print loop. The
user can activate the various NuSMV computation steps as system
commands with different options. These steps can therefore be invoked
separately, possibly undone or repeated under different
modalities. These steps include the construction of the model under
different partitioning techniques, model checking of specifications, and
the configuration of the BDD package. The interactive shell of
NuSMV is activated from the system prompt as follows
(`NuSMV>' is the default NuSMV shell prompt):
system_prompt> NuSMV -int RET NuSMV release 1.1 (compiled 30-Jul-99 at 7:25 PM) NuSMV>
A NuSMV command is a sequence of words. The first word specifies
the command to be executed. The remaining words are arguments to the
invoked command. Commands separated by a `;' are executed
sequentially; the NuSMV shell waits for each command to terminate
in turn. The behavior of commands can depend on environment variables,
similar to "csh" environment variables.
In the following we present the possible commands followed by the
related environment variables, classified in different categories. Every
command answers to the option -h by printing out the command
usage. When output is paged for some commands (option -m), it is
piped through the program specified by the UNIX PAGER shell
variable, if defined, or through UNIX command "more". Environment
variables can be assigned a value with the set command.
Command sequences to NuSMV must obey the (partial) order
specified in the figure depicted in the previous page. For instance, it
is not possible to evaluate CTL expressions before the model is built.