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

First NuSMV model check

There are several tools to apply check LTL formulas (LTL - 3, etc.). Among these, NuSMV is an open source tool that I have been using. This tool uses BDDs or SAT solvers to check properties, but I'll leave these topics for later and now focus on actual model checking a system..

In the tutorial, the following example is given:

MODULE main
VAR
request: boolean;
st: {ready, busy};
ASSIGN
init(st) := ready;
next(st) := case
              st = ready & request : busy;
              TRUE : {ready, busy};
            esac;

The given model contains two variables: request is a boolean and st - representing the state of the system - has two possible values (ready or busy).

In the ASSIGN section the initial and transition relation constraints are defined. The variable st is initialized as ready, and then for each transition:
if in the current state st is ready and there is a request, in the next state the value of st will be busy. Otherwise ("TRUE : ..."), the next value of st will be either ready or busy, non-deterministically chosen.
There are no constraints regarding initial or next values of request.

This model represents the given state machine:

The two states on the left are the initial states, since these are the states satisfying that initially st = ready.
Then, almost every transition is possible, besides when st = ready and there is a request, according to the state machine definition in the next state st must be busy.

We can check the following LTL formula:
\(\textbf{G} (st = ready \implies \textbf{X}\ st = busy)\)

That is, at any state, if st = ready, then in the next state st = busy.

To do so, we add the following to the model:

LTLSPEC
G (st = ready -> X st = busy)

Let's assume we have a file  nusmv1.smv (open with any text editor).

Now (from the command line) we can run NuSMV and check if the guarantee holds.

After having downloaded it, we can execute

NuSMV nusmv1.smv

You may need to access the whole path, for instance (in Windows)

C:\Program Files\NuSMV\bin\NuSMV nusmv1.smv

The output is the following:

-- specification  G (st = ready ->  X st = busy)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  request = 1
  st = ready
-> Input: 1.2 <-
-> State: 1.2 <-
  request = 0
  st = busy
-- Loop starts here-> State: 1.3 <-
  st = ready
-> State: 1.4 <--> Input: 1.5 <-
-> State: 1.5 <-
  st = busy
-> Input: 1.6 <-
-> State: 1.6 <-
  st = ready

In the first state of the counterexample, request is true (1) and st is ready. In the next state request is false and st is busy. So far the formula holds.
Then it is inidicated the start of the loop. This is since infinite paths are analyzed, and every counterexample includes a prefix and a loop. The first state of the loop (State 1.3) changes the value of st but not of request (only the variables changed appear). So in State 1.3 request is false and st=ready. However, in the next state st keeps being ready! Our formula is false, since there could be states when the state is ready but the next state is not busy (for instance, when there is no request).

If we change the formula and check

LTLSPEC
G ((request & st = ready) -> X st = busy)

The output obtained is:

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

LOTOS - Choice

Some time ago, I've written about the basic events in LOTOS specification (LOTOS - 1). These are given by
g?var: T \(\rightarrow\) an input of type T is expected through the gate g.
g! constant \(\rightarrow\)  an output (constant) is exposed through the gate g.

Additional operators allow building more complex processes:

Sequential composition (;)

Several events can occur in a sequence. For example, g? x: int; g!x+1 represent two events (at two different instants of time). In the first one, it is expected to synchronize on an integer input, while in the second one it is expected to synchronize on the output that is the value received plus one.

We can now define a process P with a gate g that it always receives a value and exposes the value incremented:

process P[g] =
g?x:int ; g!x+1; P[g]

The last element in the sequential composition (P[g]) indicates that a new instance of the process starts when reaching to this point.

Choice ([])

The operator Choice ([]) allows representing the choice between two (or more) paths.

For example,

g! "hello"
[]
g! "world"

allows either exposing "hello" or "world" through the gate g.

Guards ([condition] \(\rightarrow\))

In general, choice conditions are non-deterministic (or more precisely, dependent on the environment). To add conditions, we can use guards combined with the choice operator:

[condition1] \(\rightarrow\) behavior1
[]
[condition2] \(\rightarrow\) behavior2

Then, the behaviors enabled depend on the conditions. For example, let P be a process having been instantiated with a variable x

P[g](x: int)
[x <0] \(\rightarrow\) g! -x; g? y: int; P[g](y)
[]
[x >= 0] \(\rightarrow\) g! x; g? y: int; P[g](y)

This process has an if-else like behavior. It exposes the absolute value of x, receives a new value from the environment (y), and creates a new instance of the process with this value.