Interactive nusmv model checking - 2

Continuing from the last post and the model example, where we could check some LTL formulas, and see the traces, we know show how to apply interactive simulation.
This is useful for when we want to analyze different paths, and see what happens at each step, and what are the possible values of each variable at each step.

For example, we want to step over each step of a trace interactively, choosing the next step at each step.

To run NuSMV in the interactive mode we add the -int option, i.e.
NuSMV -int nusmv1.smv

Then, the NuSMV prompt appears:

NuSMV >

From now on, we will write the commands next to the prompt, but you dont need to write the prompt, just what appears after the > symbol.

The first step is to tell NuSMV to build the model, which is achieved with the command go

NuSMV > go

And now, we can check different properties. For instance:

NuSMV > check_ltlspec -p "G (st = ready -> X st = busy)"

outputs the counterexample while

NuSMV > check_ltlspec -p "G ((st = ready & request) -> X st = busy)"

outputs that the property holds:

-- specification  G ((st = ready & request) ->  X st = busy)  is true

we can check more information about the check_ltlspec option by typing

NuSMV > check_ltlspec -h

which outputs the different options for this command.

Then, we see that for a file that includes some LTL specification properties, we can check the property by number, for instance

NuSMV > check_ltlspec -n 0

To quit the command is "quit"

NuSMV > quit

In the next post I will write about simulating paths within the interactive mode.