Interactive nusmv model checking - 3

Continuing with the interactive mode of NuSMV, let's consider our example from the previous posts (nusmv1.smv).

Recall that to enter the interactive mode, we simply execute the application with the -int argument and then build the model (previous post):

NuSMV -int nusmv1.smv

NuSMV > go

Now, in order to start simulating paths, we first choose an initial state (with the pick_state command)

If you don't remember exactly how the commands are called, it is possible to type help and view all the available commands, i.e.

NuSMV > help

and then just to check that is the command we are interested in:

NuSMV > pick_state -h

We can see all the available initial states by passing the argument -i. That is,

NuSMV > pick_state -i

The output looks as follows:

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  request = TRUE
  st = ready


================= State =================
1) -------------------------
  request = FALSE

Choose a state from the above (0-1):

There are two possible states. The first one includes the values for every possible variable, while the second one includes only the valuable of request. This means that the value of st is the same as in the previous state. Let's say we choose the first state which generates a request (i.e. state 0) ).
Now by writing

NuSMV > show_traces -v

The output is

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready

we can simulate randomly other 5 steps:

NuSMV > simulate -r -k 5

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready
-> State: 1.2 <-
      request = FALSE
      st = busy
-> State: 1.3 <-
      request = TRUE
      st = ready
-> State: 1.4 <-
      request = TRUE
      st = busy
-> State: 1.5 <-
      request = FALSE
      st = ready
-> State: 1.6 <-
      request = TRUE
      st = ready

or we can be asked to interactively select the next k steps (in the example 2 steps)

NuSMV > simulate -i -k 2

So, -r represents choosing randomly, -i interactively and -k the number of steps.

An additional useful option for this command is -c which allows adding constraints that must be satisfied by the next steps. For example, we can start a new simulation path, and the condition we require is that there is a request:

NuSMV > pick_state -r -c "request"

These are the main commands and options I use for simulating paths in a model, for more options, it is always possible to use the help command (get all available commands), command -h (prints the options for any command) or revise the documentation on the site of NuSMV.