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.
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
.
%%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.
model
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.
k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k
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):
k.show('.1')
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.
k.show('.1K')
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
.
spot.contains('F"P_0.a < 2"', k)
True
*.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.
!rm -rf test1.pml
%%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:
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
model2
ltsmin model with the following variables: P_0._pc: pc P_0.a: int P_0.b: int
!rm -f test1.pml test1.pml.spins.c test1.pml.spins