Interactive nusmv model checking - 3

Continuing with the interactive mode of NuSMV, let's consider our example from the previous posts (nusmv1.smv).

Recall that to enter the interactive mode, we simply execute the application with the -int argument and then build the model (previous post):

NuSMV -int nusmv1.smv

NuSMV > go

Now, in order to start simulating paths, we first choose an initial state (with the pick_state command)

If you don't remember exactly how the commands are called, it is possible to type help and view all the available commands, i.e.

NuSMV > help

and then just to check that is the command we are interested in:

NuSMV > pick_state -h

We can see all the available initial states by passing the argument -i. That is,

NuSMV > pick_state -i

The output looks as follows:

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  request = TRUE
  st = ready


================= State =================
1) -------------------------
  request = FALSE

Choose a state from the above (0-1):

There are two possible states. The first one includes the values for every possible variable, while the second one includes only the valuable of request. This means that the value of st is the same as in the previous state. Let's say we choose the first state which generates a request (i.e. state 0) ).
Now by writing

NuSMV > show_traces -v

The output is

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready

we can simulate randomly other 5 steps:

NuSMV > simulate -r -k 5

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready
-> State: 1.2 <-
      request = FALSE
      st = busy
-> State: 1.3 <-
      request = TRUE
      st = ready
-> State: 1.4 <-
      request = TRUE
      st = busy
-> State: 1.5 <-
      request = FALSE
      st = ready
-> State: 1.6 <-
      request = TRUE
      st = ready

or we can be asked to interactively select the next k steps (in the example 2 steps)

NuSMV > simulate -i -k 2

So, -r represents choosing randomly, -i interactively and -k the number of steps.

An additional useful option for this command is -c which allows adding constraints that must be satisfied by the next steps. For example, we can start a new simulation path, and the condition we require is that there is a request:

NuSMV > pick_state -r -c "request"

These are the main commands and options I use for simulating paths in a model, for more options, it is always possible to use the help command (get all available commands), command -h (prints the options for any command) or revise the documentation on the site of NuSMV.

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.

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

Temporal Logic - LTL - 3

In this post we'll see the formal semantics of LTL (LTL - 1, LTL - 2, LTL - Literature):

The model is represented by \(\langle S, I, R, L\rangle\) where \(S\) is the set of states, \(I \subseteq S\) is the set of initial states, \(R:SxS\) is the relation transition definition and \(L: S \rightarrow 2^{AP}\) is the labeling definition where AP is the set of available atomic propositions.

In the example of the last post:

We have three states, \(S = \{s_0,s_1,s_2\}\), with \(I = \{s_0\}\), \(R = \{(s_0,s_1), (s_1,s_2), (s_2, s_2)\}\), \(L = \{s_0\mapsto\{p\},s_1\mapsto\{q\},s_2\mapsto\{p,q,r\}\}\).

A path is an infinite path \(\pi=\pi_0\pi_1\dots\) where  \(\pi_0 \in I\) and for every \(i\), \((\pi_i,\pi_{i+1})\in R\). That is, the first state of the path is an initial state of the model, and for every two consecutive states of the path, there is a relation between them.

Now we define the semantics for the boolean operations and the temporal operators we have mentioned.

\(\pi,i\vDash q\) with \(q \in AP\) if and only if \(q \in L(\pi_i)\). That is, given a path \(\pi\) and index \(i\) of a state within the path an atomic proposition \(q\) is satisfied if and only if \(q\) belongs to the labels of that state.

\(\pi,i\vDash \neg \varphi\) if and only if  \(\pi,i\not\vDash  \varphi\). That is, not a formula is satisfied if the formula itself is not satisfied.

\(\pi,i\vDash  \varphi \land \theta\) if and only if  \(\pi,i\vDash  \varphi\) and \(\pi,i\vDash  \theta\). That is, the conjunction of two linear temporal logic formulas \(\varphi,\theta\) is satisfied if and only if both formulas are satisfied.

\(\pi,i\vDash  \varphi \lor \theta\) if and only if  \(\pi,i\vDash  \varphi\) or \(\pi,i\vDash  \theta\). That is, the disjunction of two linear temporal logic formulas \(\varphi,\theta\) is satisfied if and only at least one of the formulas is satisfied.

Now, we show the semantics of the temporal operators G, F, X, U.

\(\pi,i\vDash \textbf{G}\varphi\) if and only if for every \(j\ge i\), \(\pi,j\vDash \varphi\) , that is, every path starting with every state after \(i\) satisfies \(\varphi\).

\(\pi,i\vDash \textbf{F}\varphi\) if and only if exists \(j\ge i\), \(\pi,j\vDash \varphi\) , that is, there is a state in the future such that the path starting with that state satisfies \(\varphi\).

\(\pi,i\vDash \textbf{X}\varphi\) if and only if \(\pi,i+1\vDash \varphi\) , that is, there is the next state satisfies \(\varphi\).

\(\pi,i\vDash \varphi\textbf{U}\theta\) if and only if exists \(j\ge i\), \(\pi,j\vDash \theta\) and for every \(i\le k < j\), \(\pi,k\vDash \varphi\) , that is, there is a state \(j\) in the future such that the \(\theta\) is satisfied, and every state till \(j\) (non-including) satisfies \(\varphi\).


Or semantics:

Meeting of the Sussex Border Path with Hook Street at Monckton Hook (Andy Potter) / CC BY-SA 2.0

Temporal Logic in Literature

In this post I want to put some phrases from Literature and show (possible) translation to temporal logic (LTL - 1, LTL - 2).

1)
"In such terms Mr Gradgrind always mentally introduced himself, whether to his private circle of acquaintance, or to the public in general." Charles Dickens, Hard Times, Chapter 2

Let's compare these two formulas:

\(F (MrGradgrindMentallyIntroducesHimself)\)

\(G (MrGradgrindMentallyIntroducesHimself)\)

The first one indicates that there is one state in the future in which Mr. Gradgrind mentally introduces himself. The second one indicates that this occurs at every state, matching the keyword always in the sentence.

2)
"There will be the noise of the blows of the whip, which they will give to the horses." Alexandre Dumas, The forty-Five Guardsmen, Chapter 1

Let's compare these two formulas:

\(F\ noiseBlowsOfWhip \land F\ whipToHorses\)

\(F (noiseBlowsOfWhip \land whipToHorses)\)

The first one indicates that there is a state in the future in which there is the noise of the blows of the whip, and there is state in the future in which they whip the horses, while the second one indicates a state in the future in which both things occur. Since we know that both things are related, the whip causes the noise, we know they must be at the same state, and the second formula is preciser.

3)
' This proposal met with general applause, until an old mouse got up and said: "That is all very well, but who is to bell the Cat?" ' Aesop, Aesop's fables, Belling the Cat

A first attempt could to be to write the following formula:

\(Applause \land OldMouseQuestion\)

However, this formula expresses that at the first instant of time both things occur, and the applause may happen later and even later the question. Thus, we may attempt to correct the formula as follows:

\(Applause \land F\ OldMouseQuestion\)

It is better in that it expresses that first the applause occurs and sometime in the future the question by the old mouse. However, the applause goes only to be interrupted by the old mouse (keyword: until). Then we correct it as follows:

\(Applause\ U\ OldMouseQuestion\)

Here represents that the applause goes on until the old mouse asks its question. The only ambiguous part that remains is whether the story starts with the applause or this happens at some moment in the future. Due to our additional knowledge that first there is a discussion, then the proposal to bell the cat and only then the applause, we know that this part does not occur at the first state:

\(F\ Applause\ U\ OldMouseQuestion\)

Temporal Logic - LTL - 2

In the previous post (LTL - 1), we started talking about Linear Temporal Logic, a logic that allows expressing temporal properties about every path of a model.
In particular we have observed the temporal operators (or modalities):
G (Globally)
F (Eventually)
There is a relation between these two operators: Writing that globally something (property) holds, is equivalent to saying that the negation of the property will never hold. In terms of the operators this is expressed as:
G property = not F not property
I take this opportunity to present syntax notations I will use in future posts:
not = \( \neg \)
or = \( \lor \)
and = \( \land \)
Now, other temporal operators of interest are:
X formula (at the next state formula holds)
formula1 U formula2 (formula1 holds until formula2 holds)
For example,

In the given state machine, p q and r are atomic propositions. For example, p could represent x = 1 , q represent y > 0, and r represent that z is within some range of values. These are just examples, for each system, the set of atomic propositions is defined, and with these, the state machine representing the system is built. We will consider that if an atomic proposition does not appear in a state, then that atomic proposition does not hold at that state. For example the first state satisfies \( p \land \neg q \land \neg r \).

When standing at the first state of the model in the example (let's call it M), we can see that the next state satisfies q. That is, \( M \vDash \textbf{X}\ q \). When writing that the model satisfies an LTL formula, we are saying that every path starting from the initial states of the model satisfies the formula.

We can also observe that \(M \vDash  \textbf{X}\ \neg p \) ,\( M \vDash   \neg \textbf{X}\ r \), \( M \vDash  \textbf{X} \textbf{X}\ q \), and \( M \vDash  \textbf{X} \textbf{X}\textbf{X}\ p \). Question to the reader: why?


Thus, X expresses at the next state (from the state we are currently at). For example although the model does not satisfy that at the next state of every path starting from the initial states p will hold, there exists a future state such that its next state will satify p. That is \( M \vDash \textbf{F}\textbf{X}\ p \). And this way the different temporal operators can be combined.

cc license from origin

The remaining operator for this post is U: The idea is that a formula "formula1 U formula2" is satisfied when formula1 holds at every state until some state where formula2 holds. If formula2 holds, then the formula with until holds. If formula2 never holds, then the until formula is not satisifed. In the next blog we will give the more formal definitions of the temporal operators (or modalities) and understand why the express the general idea we have seen in these two posts.

Temporal Logic - LTL - 1

Temporal logic allows expressing properties that a system should satisfy along time. We will first talk about linear temporal logic which expresses properties over every possible path. For example, let's consider the following model:

Let r be the proposition representing that the system is running and h the proposition representing the the system has halted.

Then we could check whether it always holds that this system will always halt. According to the state machine representation this is false: We can consider the path r,r,r,r,... and never get to the halt state.

With linear temporal logic we can express the property "the system will always halt" and other properties referring to time.

For example, the operator G formula (globally) indicates that from a given state, every state state satisfies formula (formula can be any linear temporal logic formula.

For instance, the formula G (r or h) is true. Every state of every path starting from the initial state satisfies that r or h hold. However, the formula G r is not satisfied by every path.

The operator F formula indicates that formula will be true at some state in the future.

The given example does not satisfy F h (because of the given counterexample where the second state is not reached..

However the formula F r, holds (a state satisfying r is reached at the first state)

In future posts we will consider some other examples and other operators.