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