Interactive nusmv model checking - 1

In the last post we saw about model checking LTL formulas with NuSMV by writing the model, the formula to be satisfied, and calling the program from the command line. We will now see a few things useful to interact with the model.

if we run NuSMV with the option -int, NuSMV remains open to ask commands.

We can execute:

NuSMV -int nusmv1.smv

After the header including the NuSMV version, the prompt appears:

NuSMV >

In the next lines this prompt (NuSMV > ) will appear to show where the commands go, but you don't have to write it. We can now write go so that the model is built. That is,

NuSMV > go

And now we can check formulas. For example,

NuSMV > check_ltlspec -p "G st = ready"

outputs a counterexample, while

NuSMV > check_ltlspec -p "st = ready"

indicating that in the first state st is ready, is true.

NuSMV > show_traces 1

shows the first trace (the counterexample to "G st = ready"

At any moment we can use

NuSMV > help
to  see all the available commands

and command -h  to see the options of a command for instance

NuSMV > check_ltlspec -h

Finally we use the quit command to exit.

NuSMV > quit