Next: The NUSMV batch mode
Up: The interaction with NUSMV
Previous: The interaction with NUSMV
The NUSMV interactive shell
In this mode the system 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.
These steps include the construction of the model in different ways and the
model checking of specifications.
The NUSMV interactive shell allows for the full configuration of the
BDD options. For instance, several automatic variable ordering
methods and cache configuration mechanisms can be suitably tuned
according to the application.
Moreover, the NUSMV interactive shell provides the user with a script
language that makes it possible to define different model checking
algorithms that can be invoked as model checking tactics. These
algorithms are provided via parameterized scripts.
The interactive shell of NUSMV is activated from the system prompt as
follows (``NuSMV>'' is the default prompt that NUSMV prints out
to indicate that it is ready to evaluate commands):
system_prompt> NuSMV -int
NuSMV release 1.0 (compiled 11-Nov-98 at 8:28 PM)
In Figure 6 we can see a typical
interaction with NUSMV through the interactive shell.5 The file
``counter.smv'' contains the example depicted in
Figure 4. The verification process in NUSMV can be
decomposed into the following sequence of basic steps.
A typical interaction with NuSMV via the interactive shell. NuSMV
commands are in boldface.
- The first step towards verification is reading the model. This
is performed by typing the NUSMV command read_model. This
command takes as argument a file name containing the model
specification. After the correct execution of this command an
internal representation of the read file is built and stored.
- The second step consists in transforming the hierarchical
description into a flattened description. This is performed by typing
the command flatten_hierarchy. After the correct
execution of this command all the information needed to build
the automaton is separated out (e.g., the variable names,
their range, a symbolic representation of the initial states
and of the transition relation of the flattened system).
- The third step consists in the encoding of the scalar
variables into boolean variables. The
responsible for this task. It takes an optional argument
specifying a file containing the ordering in which the
variables have to be built.6 As a default, the order of variables used by NUSMV
corresponds to the order in which the variables appear in a
depth first traversal of the hierarchy .
- The fourth step consists of the compilation of the structures
built by the flatten_hierarchy into BDDs using the
encoding performed by build_variables. During this step
some checks are performed that avoid circular dependencies in
assignments and multiple definitions . The
NUSMV command that implements this step is
build_model. This command has an option specifying
the partitioning method to be used, i.e. monolithic,
conjunctive, or disjunctive (see Section
4). It is possible to build first the
transition relation in different formats and then choose the
most appropriate to the specific problem.
- The fifth step deals with the fairness
constraints . This command can be executed only
when all the previous commands have been executed. This is due
to the fact that fairness constraints are CTL
formulas whose evaluation uses a previously computed
After these five steps, the internal representation of the
automaton is available to perform model checking.
- It is possible to compute the set of reachable states, via the
compute_reachable command. This allows the user to simplify
the evaluation of all the specifications by restricting the search
only to reachable states.
- It is possible to start the verification of CTL
specifications (via the check_spec command), of LTL
specifications (via the check_ltlspec command), and of
invariants (via the check_invar command). All these
commands, if called with no arguments, apply to the
specifications of the respective type, if any, listed in the
source file. Optionally a CTL, LTL or propositional formula
can be given as an argument.
In the transcript of Figure 6 first we check the
property AG AF bit2.carry_out (the execution of
check_spec without arguments, thus verifying the properties
listed in the input file). Then we check the property AG AX
bit2.carry_out (invariantly in the next state
bit2.carry_out is 1). This property appear to be
false and a counterexample exploiting why the formula is not verified
is computed and printed out.