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 tmpwot5yb9c.pml...
Parsing tmpwot5yb9c.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/tmpwot5yb9c.pml.spins.c
Compiled C code to PINS library tmpwot5yb9c.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]:
b'\n\n\nt\n[all]\n\n\n\n0\n\nP_0._pc=0, P_0.a=0, P_0.b=0\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\nI->0\n\n\n\n\n\n1\n\nP_0._pc=0, P_0.a=1, P_0.b=0\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n0->1\n\n\n\n\n\n2\n\nP_0._pc=0, P_0.a=0, P_0.b=1\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n0->2\n\n\n\n\n\n3\n\nP_0._pc=0, P_0.a=2, P_0.b=0\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n1->3\n\n\n\n\n\n4\n\nP_0._pc=0, P_0.a=1, P_0.b=1\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n1->4\n\n\n\n\n\n2->4\n\n\n\n\n\n5\n\nP_0._pc=0, P_0.a=0, P_0.b=2\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n2->5\n\n\n\n\n\n6\n\nP_0._pc=0, P_0.a=3, P_0.b=0\n!"P_0.a < 2" & !"P_0.b > 1" & dead\n\n\n\n3->6\n\n\n\n\n\n7\n\nP_0._pc=0, P_0.a=2, P_0.b=1\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n3->7\n\n\n\n\n\n4->7\n\n\n\n\n\n8\n\nP_0._pc=0, P_0.a=1, P_0.b=2\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n4->8\n\n\n\n\n\n5->8\n\n\n\n\n\n9\n\nP_0._pc=0, P_0.a=0, P_0.b=3\n"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n5->9\n\n\n\n\n\n6->6\n\n\n\n\n\n10\n\nP_0._pc=0, P_0.a=3, P_0.b=1\n!"P_0.a < 2" & !"P_0.b > 1" & dead\n\n\n\n7->10\n\n\n\n\n\n11\n\nP_0._pc=0, P_0.a=2, P_0.b=2\n!"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n7->11\n\n\n\n\n\n8->11\n\n\n\n\n\n12\n\nP_0._pc=0, P_0.a=1, P_0.b=3\n"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n8->12\n\n\n\n\n\n9->9\n\n\n\n\n\n10->10\n\n\n\n\n\n13\n\nP_0._pc=0, P_0.a=3, P_0.b=2\n!"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n11->13\n\n\n\n\n\n14\n\nP_0._pc=0, P_0.a=2, P_0.b=3\n!"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n11->14\n\n\n\n\n\n12->12\n\n\n\n\n\n13->13\n\n\n\n\n\n14->14\n\n\n\n\n\n'

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]:
b'\n\n\nt\n[all]\n\n\n\n0\n\n\n0\n\n\n\n\n\nI->0\n\n\n\n\n\n1\n\n\n1\n\n\n\n\n\n0->1\n\n\n\n\n\n2\n\n\n2\n\n\n\n\n\n0->2\n\n\n\n\n\n3\n\n\n3\n\n\n\n\n\n1->3\n\n\n\n\n\n4\n\n\n4\n\n\n\n\n\n1->4\n\n\n\n\n\n2->4\n\n\n\n\n\n5\n\n\n5\n\n\n\n\n\n2->5\n\n\n\n\n\n6\n\n\n6\n\n\n\n\n\n3->6\n\n\n\n\n\n7\n\n\n7\n\n\n\n\n\n3->7\n\n\n\n\n\n4->7\n\n\n\n\n\n8\n\n\n8\n\n\n\n\n\n4->8\n\n\n\n\n\n5->8\n\n\n\n\n\n9\n\n\n9\n\n\n\n\n\n5->9\n\n\n\n\n\n6->6\n\n\n\n\n\n10\n\n\n10\n\n\n\n\n\n7->10\n\n\n\n\n\n11\n\n\n11\n\n\n\n\n\n7->11\n\n\n\n\n\n8->11\n\n\n\n\n\n12\n\n\n12\n\n\n\n\n\n8->12\n\n\n\n\n\n9->9\n\n\n\n\n\n10->10\n\n\n\n\n\n13\n\n\n13\n\n\n\n\n\n11->13\n\n\n\n\n\n14\n\n\n14\n\n\n\n\n\n11->14\n\n\n\n\n\n12->12\n\n\n\n\n\n13->13\n\n\n\n\n\n14->14\n\n\n\n\n\n'

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]:
b'\n\n\nt\n[all]\n\n\n\n0\n\n\n0\n\n\n\n\n\nI->0\n\n\n\n\n\n1\n\n\n1\n\n\n\n\n\n0->1\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n2\n\n\n2\n\n\n\n\n\n0->2\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n3\n\n\n3\n\n\n\n\n\n1->3\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n4\n\n\n4\n\n\n\n\n\n1->4\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n2->4\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n5\n\n\n5\n\n\n\n\n\n2->5\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n6\n\n\n6\n\n\n\n\n\n3->6\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n7\n\n\n7\n\n\n\n\n\n3->7\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n4->7\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n8\n\n\n8\n\n\n\n\n\n4->8\n\n\n"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n5->8\n\n\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n9\n\n\n9\n\n\n\n\n\n5->9\n\n\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n6->6\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & dead\n\n\n\n10\n\n\n10\n\n\n\n\n\n7->10\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n11\n\n\n11\n\n\n\n\n\n7->11\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & !dead\n\n\n\n8->11\n\n\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n12\n\n\n12\n\n\n\n\n\n8->12\n\n\n"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n9->9\n\n\n"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n10->10\n\n\n!"P_0.a < 2" & !"P_0.b > 1" & dead\n\n\n\n13\n\n\n13\n\n\n\n\n\n11->13\n\n\n!"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n14\n\n\n14\n\n\n\n\n\n11->14\n\n\n!"P_0.a < 2" & "P_0.b > 1" & !dead\n\n\n\n12->12\n\n\n"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n13->13\n\n\n!"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n14->14\n\n\n!"P_0.a < 2" & "P_0.b > 1" & dead\n\n\n\n'

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