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.
