In [1]:
import spot
import spot.ltsmin
# The following line causes the notebook to exit with 77 if spins is not 
# installed, therefore skipping this test in the test suite.
spot.ltsmin.require('spins')
spot.setup()

There are two ways to load a Promela model: from a file or from a cell.

Loading from a cell

Using the %%pml magic will save the model in a temporary file, call spins to compile it, load the resulting shared library, and store the result into an object whose name is passed as an argument to %%pml.

In [2]:
%%pml model
active proctype P() {
int a = 0;
int b = 0;
x: if
  :: d_step {a < 3 && b < 3; a = a + 1; } goto x;
  :: d_step {a < 3 && b < 3; b = b + 1; } goto x;
fi;
}

SpinS Promela Compiler - version 1.1 (3-Feb-2015)
(C) University of Twente, Formal Methods and Tools group

Parsing tmpl3q0izvh.pml...
Parsing tmpl3q0izvh.pml done (0.0 sec)

Optimizing graphs...
   StateMerging changed 0 states/transitions.
   RemoveUselessActions changed 2 states/transitions.
   RemoveUselessGotos changed 2 states/transitions.
   RenumberAll changed 1 states/transitions.
Optimization done (0.0 sec)

Generating next-state function ...
   Instantiating processes
   Statically binding references
   Creating transitions
Generating next-state function done (0.0 sec)

Creating state vector
Creating state labels
Generating transitions/state dependency matrices (2 / 3 slots) ... 
   Found          5 /         15 ( 33.3%) Guard/slot reads               
   Found          6 /          6 (100.0%) Transition/slot tests               
   Found         2,         4,         4 /        18 ( 11.1%,  22.2%,  22.2%) Actions/slot r,W,w               
   Found         2,         4,         4 /         6 ( 33.3%,  66.7%,  66.7%) Atomics/slot r,W,w               
   Found         6,         4,         4 /         6 (100.0%,  66.7%,  66.7%) Transition/slot r,W,w               
Generating transition/state dependency matrices done (0.0 sec)

Generating guard dependency matrices (5 guards) ...
   Found          3 /         12 ( 25.0%) Guard/guard dependencies               
   Found          8 /         10 ( 80.0%) Transition/guard writes               

   Found          4 /          4 (100.0%) Transition/transition writes               
   Found          2 /         12 ( 16.7%) !MCE guards               
   Found          1 /          2 ( 50.0%) !MCE transitions               
   Found          7 /         25 ( 28.0%) !ICE guards               
   Found         10 /         10 (100.0%) !NES guards               
   Found          4 /          4 (100.0%) !NES transitions               
   Found          8 /         10 ( 80.0%) !NDS guards               
   Found          0 /         10 (  0.0%) MDS guards               
   Found          4 /         10 ( 40.0%) MES guards               
   Found          0 /          4 (  0.0%) !NDS transitions               
   Found          0 /          2 (  0.0%) !DNA transitions               
   Found          2 /          2 (100.0%) Commuting actions               
Generating guard dependency matrices done (0.0 sec)

Written C code to /home/adl/git/spot/tests/python/tmpl3q0izvh.pml.spins.c
Compiled C code to PINS library tmpl3q0izvh.pml.spins

Yes, the spins compiler is quite verbose. Printing the resulting model object will show information about the variables in that model.

In [3]:
model
Out[3]:
ltsmin model with the following variables:
  P_0._pc: pc
  P_0.a: int
  P_0.b: int

To instantiate a Kripke structure, one should provide a list of atomic proposition to observe.

In [4]:
k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k
Out[4]:
t [all] 0 P_0._pc=0, P_0.a=0, P_0.b=0 "P_0.a < 2" & !"P_0.b > 1" & !dead I->0 1 P_0._pc=0, P_0.a=1, P_0.b=0 "P_0.a < 2" & !"P_0.b > 1" & !dead 0->1 2 P_0._pc=0, P_0.a=0, P_0.b=1 "P_0.a < 2" & !"P_0.b > 1" & !dead 0->2 3 P_0._pc=0, P_0.a=2, P_0.b=0 !"P_0.a < 2" & !"P_0.b > 1" & !dead 1->3 4 P_0._pc=0, P_0.a=1, P_0.b=1 "P_0.a < 2" & !"P_0.b > 1" & !dead 1->4 2->4 5 P_0._pc=0, P_0.a=0, P_0.b=2 "P_0.a < 2" & "P_0.b > 1" & !dead 2->5 6 P_0._pc=0, P_0.a=3, P_0.b=0 !"P_0.a < 2" & !"P_0.b > 1" & dead 3->6 7 P_0._pc=0, P_0.a=2, P_0.b=1 !"P_0.a < 2" & !"P_0.b > 1" & !dead 3->7 4->7 8 P_0._pc=0, P_0.a=1, P_0.b=2 "P_0.a < 2" & "P_0.b > 1" & !dead 4->8 5->8 9 P_0._pc=0, P_0.a=0, P_0.b=3 "P_0.a < 2" & "P_0.b > 1" & dead 5->9 6->6 10 P_0._pc=0, P_0.a=3, P_0.b=1 !"P_0.a < 2" & !"P_0.b > 1" & dead 7->10 11 P_0._pc=0, P_0.a=2, P_0.b=2 !"P_0.a < 2" & "P_0.b > 1" & !dead 7->11 8->11 12 P_0._pc=0, P_0.a=1, P_0.b=3 "P_0.a < 2" & "P_0.b > 1" & dead 8->12 9->9 10->10 13 P_0._pc=0, P_0.a=3, P_0.b=2 !"P_0.a < 2" & "P_0.b > 1" & dead 11->13 14 P_0._pc=0, P_0.a=2, P_0.b=3 !"P_0.a < 2" & "P_0.b > 1" & dead 11->14 12->12 13->13 14->14

And then from this Kripke structure you can do some model checking using the same functions as illustrated in ltsmin-dve.ipynb.

For displaying Kripke structures more compactly, it can be useful to use option 1 to move all state labels in tooltips (mouse over the state to see them):

In [5]:
k.show('.1')
Out[5]:
t [all] 0 0 I->0 1 1 0->1 2 2 0->2 3 3 1->3 4 4 1->4 2->4 5 5 2->5 6 6 3->6 7 7 3->7 4->7 8 8 4->8 5->8 9 9 5->9 6->6 10 10 7->10 11 11 7->11 8->11 12 12 8->12 9->9 10->10 13 13 11->13 14 14 11->14 12->12 13->13 14->14

Another option is to use option K to disable to state-labeling (that is enabled by default for Kripke structure) and use transition-labeling instead. Combining with 1, this will preserve the state's data as a tooltip.

In [6]:
k.show('.1K')
Out[6]:
t [all] 0 0 I->0 1 1 0->1 "P_0.a < 2" & !"P_0.b > 1" & !dead 2 2 0->2 "P_0.a < 2" & !"P_0.b > 1" & !dead 3 3 1->3 "P_0.a < 2" & !"P_0.b > 1" & !dead 4 4 1->4 "P_0.a < 2" & !"P_0.b > 1" & !dead 2->4 "P_0.a < 2" & !"P_0.b > 1" & !dead 5 5 2->5 "P_0.a < 2" & !"P_0.b > 1" & !dead 6 6 3->6 !"P_0.a < 2" & !"P_0.b > 1" & !dead 7 7 3->7 !"P_0.a < 2" & !"P_0.b > 1" & !dead 4->7 "P_0.a < 2" & !"P_0.b > 1" & !dead 8 8 4->8 "P_0.a < 2" & !"P_0.b > 1" & !dead 5->8 "P_0.a < 2" & "P_0.b > 1" & !dead 9 9 5->9 "P_0.a < 2" & "P_0.b > 1" & !dead 6->6 !"P_0.a < 2" & !"P_0.b > 1" & dead 10 10 7->10 !"P_0.a < 2" & !"P_0.b > 1" & !dead 11 11 7->11 !"P_0.a < 2" & !"P_0.b > 1" & !dead 8->11 "P_0.a < 2" & "P_0.b > 1" & !dead 12 12 8->12 "P_0.a < 2" & "P_0.b > 1" & !dead 9->9 "P_0.a < 2" & "P_0.b > 1" & dead 10->10 !"P_0.a < 2" & !"P_0.b > 1" & dead 13 13 11->13 !"P_0.a < 2" & "P_0.b > 1" & !dead 14 14 11->14 !"P_0.a < 2" & "P_0.b > 1" & !dead 12->12 "P_0.a < 2" & "P_0.b > 1" & dead 13->13 !"P_0.a < 2" & "P_0.b > 1" & dead 14->14 !"P_0.a < 2" & "P_0.b > 1" & dead

Since a kripke structure is a twa, can be used on the right-hand side of contains. Here we show that every path of k contains a step where P_0.a < 2.

In [7]:
spot.contains('F"P_0.a < 2"', k)
Out[7]:
True

Loading from a *.pml file

Another option is to use ltsmin.load() to load a Promela file directly. In order for this test-case to be self-contained, we are going to write the Promela file first, but in practice you probably already have your model.

In [8]:
!rm -rf test1.pml
In [9]:
%%file test1.pml
active proctype P() {
int a = 0;
int b = 0;
x: if
  :: d_step {a < 3 && b < 3; a = a + 1; } goto x;
  :: d_step {a < 3 && b < 3; b = b + 1; } goto x;
fi;
}

Writing test1.pml

Now load it:

In [10]:
model2 = spot.ltsmin.load('test1.pml')

SpinS Promela Compiler - version 1.1 (3-Feb-2015)
(C) University of Twente, Formal Methods and Tools group

Parsing test1.pml...
Parsing test1.pml done (0.0 sec)

Optimizing graphs...
   StateMerging changed 0 states/transitions.
   RemoveUselessActions changed 2 states/transitions.
   RemoveUselessGotos changed 2 states/transitions.
   RenumberAll changed 1 states/transitions.
Optimization done (0.0 sec)

Generating next-state function ...
   Instantiating processes
   Statically binding references
   Creating transitions
Generating next-state function done (0.0 sec)

Creating state vector
Creating state labels
Generating transitions/state dependency matrices (2 / 3 slots) ... 
   Found          5 /         15 ( 33.3%) Guard/slot reads               
   Found          6 /          6 (100.0%) Transition/slot tests               
   Found         2,         4,         4 /        18 ( 11.1%,  22.2%,  22.2%) Actions/slot r,W,w               
   Found         2,         4,         4 /         6 ( 33.3%,  66.7%,  66.7%) Atomics/slot r,W,w               
   Found         6,         4,         4 /         6 (100.0%,  66.7%,  66.7%) Transition/slot r,W,w               
Generating transition/state dependency matrices done (0.0 sec)

Generating guard dependency matrices (5 guards) ...
   Found          3 /         12 ( 25.0%) Guard/guard dependencies               
   Found          8 /         10 ( 80.0%) Transition/guard writes               

   Found          4 /          4 (100.0%) Transition/transition writes               
   Found          2 /         12 ( 16.7%) !MCE guards               
   Found          1 /          2 ( 50.0%) !MCE transitions               
   Found          7 /         25 ( 28.0%) !ICE guards               
   Found         10 /         10 (100.0%) !NES guards               
   Found          4 /          4 (100.0%) !NES transitions               
   Found          8 /         10 ( 80.0%) !NDS guards               
   Found          0 /         10 (  0.0%) MDS guards               
   Found          4 /         10 ( 40.0%) MES guards               
   Found          0 /          4 (  0.0%) !NDS transitions               
   Found          0 /          2 (  0.0%) !DNA transitions               
   Found          2 /          2 (100.0%) Commuting actions               
Generating guard dependency matrices done (0.0 sec)

Written C code to /home/adl/git/spot/tests/python/test1.pml.spins.c
Compiled C code to PINS library test1.pml.spins
In [11]:
model2
Out[11]:
ltsmin model with the following variables:
  P_0._pc: pc
  P_0.a: int
  P_0.b: int
In [12]:
!rm -f test1.pml test1.pml.spins.c test1.pml.spins