Go to the first, previous, next, last section, table of contents.
To give the user the opportunity to get familiar with the behavior of the model
to be checked, a simulation feature has been provided in the NuSMV system.
A simulation's facility lets the user widely navigate structures and properties
of the model under test through the generation of its possible executions (traces
from now on). It also allows the user to acquire confidence with the
correctness of the model before actual verification of properties. Maximum
flexibility and degrees of freedom in a simulation session are achieved introducing
three different trace generation policies: deterministic, random and interactive.
Each of them corresponds to a different way a state is chosen from a set.
In deterministic simulation mode the first state of a set (whatever it is) is
chosen, while in the random one the choice is non deterministically performed.
In these two first modes traces are automatically generated by NuSMV:
the user obtains the whole of the trace in a time without control over the generation
itself (except for the simulation mode and the number of states entered via
command line).
Third simulation mode lets the user have a complete control over traces generation
by interactively building the trace. During an interactive simulation session,
the system stops at every step showing a list of possible future states: the
user is requested to choose one of the items. This feature is particularly
useful when one wants to inspect some particular reactions of the model to
be checked.
To avoid that the user easily gets confused when the number of possible choices
is too high, an internal limit on the number of states that are showed step by
step has been set. If, eventually, such a situation should take place, the system
will ask the user to "guide" the simulation via the insertion of some further
constraints (as simple expressions) over the variables.
The system will continue to ask for constraints insertion until the number of
future states will be under a predefined threshold: expressions entered during
this particular phase are accumulated (in a logical product) in a single big constraint
used only for the actual step of the simulation and discarded before the next one.
The system also makes a control over the expressions given by the user and will
request for a further insertion if an inconsistency arises.
Cases of inconsistency (i.e. empty set of states) may be located in:
It is also possible to specify some constraints as a command line parameter: these expressions will be considered in all of the simulation steps. If entered constraints were too strong an execution may not exist, simulation stops in the last found state and the trace generated until that point is stored in the system (see also command descriptions below).
Every trace generated during a NuSMV session (created either by the
counterexample generator or by the simulator itself) can be explored in a second
time via the show_traces command or the goto_state
command (see section 4.4 Traces Inspection Commands).
Commands descriptions follow:
simulate
command (see below).
The state can be chosen according to different policies which can
be specified via command line options. By default the state is chosen
in a deterministic way.
-i
option has been choosen.
PAGER shell
variable if defined, else through UNIX "more" command.
pick_state or goto_state commands). It is possible to run the
simulation in three ways (according to different command line policies):
deterministic (the default mode) random and interactive.
The resulting sequence is stored in a trace indexed with an integer number
taking into account the total number of traces stored in the system. There is
a different behavior in the way traces are builded, according to how
current state is set: current state is always put at the beginning
of a new trace (so it will contain at most steps + 1 states) except when it is
the last state of an existent old one. In this case the old trace is
lengthened by at most steps states.
pick_state command,
or during an interactive simulation session (when the number of future states to
be displayed is too high), that are "local" only to a single step of the
simulation and are "forgotten" in the next one
-i
option has been choosen.
A typical execution sequence of a simulation session could be as follows:
suppose
to use the model described below (2).
MODULE main
VAR
request : boolean;
state : {ready,busy};
ASSIGN
init(state) := ready;
next(state) := case
state = ready & request : busy;
1 : {ready,busy};
esac;
SPEC
AG(request -> AF state = busy)
This model has now to be read into the NuSMV system
(3) (see section 4.1 Model Reading and Building).
A starting point (i.e. a state) is needed before the simulator could start
to build any trace. By default the simulator gets the actual current state
as a starting point of every new trace: so it will be included as the first state
of a new trace except if otherwise stated; the user has been provided with
the following two NuSMV commands to overcome this behavior:
goto_state: this command (see section 4.4 Traces Inspection Commands)
provides the user to set any state of any already existent trace as the
current state;
pick_state: this command can be used whenever one wants to choose the
starting point of a new trace among the set of initial states, and it has to be
used when a current state doesn't exist yet (that is when the system has being
reset).
As at this point of the example current state doesn't exist, and there
is no trace currently stored in the system, an item from the set of initial states
has to be picked using the NuSMV pick_state command.
A simulation session can be started now, using the simulate command.
The system will generate a trace according to the options entered
via command line (4).
New builded traces are numbered: every trace is identified by an integer
number, while every state belonging to a trace is identified by a dot
notation: for example state 1.3 is the third state of the first generated
trace.
system_prompt> NuSMV -int short.smv
NuSMV release 1.1 (compiled 30-Jul-99 at 7:25 PM)
NuSMV > go
NuSMV > pick_state -r
NuSMV > print_current_state -v
Current state is 1.1
request = 0
state = ready
NuSMV > simulate -r 3
********* Starting Simulation From State 1.1 *********
NuSMV > show_traces -t
There is 1 trace currently available.
NuSMV > show_traces -v
#################### Trace number: 1 ####################
-> State 1.1 <-
request = 0
state = ready
-> State 1.2 <-
request = 1
state = busy
-> State 1.3 <-
request = 1
state = ready
-> State 1.4 <-
request = 1
state = busy
All that the user has to do to change the starting point of the next new
trace is to use the pick_state or the goto_state commands
(5).
Note that in the next example trace 1 has been lengthened as current state
was set to the last state of an existing trace.
NuSMV > goto_state 1.4
request = 1
state = busy
NuSMV > simulate -r 3
********* Starting Simulation From State 1.4 *********
NuSMV > show_traces 1
#################### Trace number: 1 ####################
-> State 1.1 <-
request = 0
state = ready
-> State 1.2 <-
request = 1
state = busy
-> State 1.3 <-
state = ready
-> State 1.4 <-
state = busy
-> State 1.5 <-
state = ready
-> State 1.6 <-
request = 0
state = busy
-> State 1.7 <-
request = 1
The user is also able to interactively choose the states of the trace he wants to build: an example of an interactive picking of an initial state is showed below:
NuSMV > pick_state -i -a
*************** AVAILABLE FUTURE STATES ***************
0) -------------------------
request = 0
state = ready
1) -------------------------
request = 1
state = ready
Choose a state from the above (0-1): 1 RET
Chosen state is: 1
request = 1
state = ready
Furthermore, the user is able to specify some constraints to restrict sets
of states from which the simulator will pick out. Constraints can be
set for both the pick_state command and the simulate command.
For the simulate command these constraints are "global" for the actual
trace to be generated, in the sense that they are always included in every step
of the simulation. They are therefore to be intended in an opposite way with
respect to those constraints eventually entered togheter with the pick_state
command, or during an interactive simulation session (when the number of future
states to be displayed is too high), that are "local" only to a single step of the
simulation and are "forgotten" in the next one. For example lets pick an initial
state with some simple constraints:
NuSMV > pick_state -c "request = 1" -i
*************** AVAILABLE FUTURE STATES ***************
0) -------------------------
request = 1
state = ready
There's only one future state. Press Return to Proceed. RET
Chosen state is: 0
request = 1
state = ready
Note how the set of possible states to choose has being restricted (in this case there is only one future state, so the system will automatically pick it, waiting for the user to press the RET key).