In [1]:
import spot
import spot.ltsmin
# The following line causes the notebook to exit with 77 if divine is not 
# installed, therefore skipping this test in the test suite.
spot.ltsmin.require('divine')
# This is notebook also tests the limitation of the number of states in the GraphViz output
spot.setup(max_states=10)

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

Loading from a file

We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file.

In [2]:
!rm -f test1.dve
In [3]:
%%file test1.dve
int a = 0, b = 0;

process P {
 state x;
 init x;

 trans
   x -> x { guard a < 3 && b < 3; effect a = a + 1; },
   x -> x { guard a < 3 && b < 3; effect b = b + 1; };
}

process Q {
  state wait, work;
  init wait;
  trans
    wait -> work { guard b > 1; },
    work -> wait { guard a > 1; };
}

system async;
Writing test1.dve

The spot.ltsmin.load function compiles the model using the ltlmin interface and load it. This should work with DiVinE models if divine --LTSmin works, and with Promela models if spins is installed.

In [4]:
m = spot.ltsmin.load('test1.dve')

Compiling the model creates all several kinds of files. The test1.dve file is converted into a C++ source code test1.dve.cpp which is then compiled into a shared library test1.dve2c. Becauce spot.ltsmin.load() has already loaded this shared library, all those files can be erased. If you do not erase the files, spot.ltsmin.load() will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.

For editing and loading DVE file from a notebook, it is a better to use the %%dve as shown next.

In [5]:
!rm -f test1.dve test1.dve.cpp test1.dve2C

Loading from a notebook cell

The %%dve cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files). The variable name that should receive the model (here m) should be indicated on the first line, after %dve.

In [6]:
%%dve m
int a = 0, b = 0;

process P {
 state x;
 init x;

 trans
   x -> x { guard a < 3 && b < 3; effect a = a + 1; },
   x -> x { guard a < 3 && b < 3; effect b = b + 1; };
}

process Q {
  state wait, work;
  init wait;
  trans
    wait -> work { guard b > 1; },
    work -> wait { guard a > 1; };
}

system async;

Working with an ltsmin model

Printing an ltsmin model shows some information about the variables it contains and their types, however the info() methods provide the data in a map that is easier to work with.

In [7]:
m
Out[7]:
ltsmin model with the following variables:
  a: int
  b: int
  P: ['x']
  Q: ['wait', 'work']
In [8]:
sorted(m.info().items())
Out[8]:
[('state_size', 4),
 ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),
 ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]

To obtain a Kripke structure, call kripke and supply a list of atomic propositions to observe in the model.

In [9]:
k = m.kripke(["a<1", "b>2"])
k
Out[9]:
t [all] 0 a=0, b=0, Q=0 "a<1" & !"b>2" & !dead I->0 1 a=1, b=0, Q=0 !"a<1" & !"b>2" & !dead 0->1 2 a=0, b=1, Q=0 "a<1" & !"b>2" & !dead 0->2 3 a=2, b=0, Q=0 !"a<1" & !"b>2" & !dead 1->3 4 a=1, b=1, Q=0 !"a<1" & !"b>2" & !dead 1->4 2->4 5 a=0, b=2, Q=0 "a<1" & !"b>2" & !dead 2->5 6 a=3, b=0, Q=0 !"a<1" & !"b>2" & dead 3->6 7 a=2, b=1, Q=0 ... 3->7 4->7 8 a=1, b=2, Q=0 ... 4->8 5->8 u5 ... 5->u5 9 a=0, b=3, Q=0 ... 5->9 6->6 u7 ... 7->u7 u8 ... 8->u8 u9 ... 9->u9
In [10]:
k.show('.<15')
Out[10]:
t [all] 0 a=0, b=0, Q=0 "a<1" & !"b>2" & !dead I->0 1 a=1, b=0, Q=0 !"a<1" & !"b>2" & !dead 0->1 2 a=0, b=1, Q=0 "a<1" & !"b>2" & !dead 0->2 3 a=2, b=0, Q=0 !"a<1" & !"b>2" & !dead 1->3 4 a=1, b=1, Q=0 !"a<1" & !"b>2" & !dead 1->4 2->4 5 a=0, b=2, Q=0 "a<1" & !"b>2" & !dead 2->5 6 a=3, b=0, Q=0 !"a<1" & !"b>2" & dead 3->6 7 a=2, b=1, Q=0 !"a<1" & !"b>2" & !dead 3->7 4->7 8 a=1, b=2, Q=0 !"a<1" & !"b>2" & !dead 4->8 5->8 9 a=0, b=3, Q=0 ... 5->9 10 a=0, b=2, Q=1 "a<1" & !"b>2" & !dead 5->10 6->6 11 a=3, b=1, Q=0 !"a<1" & !"b>2" & dead 7->11 12 a=2, b=2, Q=0 ... 7->12 8->12 13 a=1, b=3, Q=0 ... 8->13 14 a=1, b=2, Q=1 ... 8->14 u9 ... 9->u9 10->14 u10 ... 10->u10 11->11 u12 ... 12->u12 u13 ... 13->u13 u14 ... 14->u14
In [11]:
k.show('.<0')  # unlimited output
Out[11]:
t [all] 0 a=0, b=0, Q=0 "a<1" & !"b>2" & !dead I->0 1 a=1, b=0, Q=0 !"a<1" & !"b>2" & !dead 0->1 2 a=0, b=1, Q=0 "a<1" & !"b>2" & !dead 0->2 3 a=2, b=0, Q=0 !"a<1" & !"b>2" & !dead 1->3 4 a=1, b=1, Q=0 !"a<1" & !"b>2" & !dead 1->4 2->4 5 a=0, b=2, Q=0 "a<1" & !"b>2" & !dead 2->5 6 a=3, b=0, Q=0 !"a<1" & !"b>2" & dead 3->6 7 a=2, b=1, Q=0 !"a<1" & !"b>2" & !dead 3->7 4->7 8 a=1, b=2, Q=0 !"a<1" & !"b>2" & !dead 4->8 5->8 9 a=0, b=3, Q=0 "a<1" & "b>2" & !dead 5->9 10 a=0, b=2, Q=1 "a<1" & !"b>2" & !dead 5->10 6->6 11 a=3, b=1, Q=0 !"a<1" & !"b>2" & dead 7->11 12 a=2, b=2, Q=0 !"a<1" & !"b>2" & !dead 7->12 8->12 13 a=1, b=3, Q=0 !"a<1" & "b>2" & !dead 8->13 14 a=1, b=2, Q=1 !"a<1" & !"b>2" & !dead 8->14 15 a=0, b=3, Q=1 "a<1" & "b>2" & dead 9->15 10->14 10->15 11->11 16 a=3, b=2, Q=0 !"a<1" & !"b>2" & !dead 12->16 17 a=2, b=3, Q=0 !"a<1" & "b>2" & !dead 12->17 18 a=2, b=2, Q=1 !"a<1" & !"b>2" & !dead 12->18 19 a=1, b=3, Q=1 !"a<1" & "b>2" & dead 13->19 14->18 14->19 15->15 20 a=3, b=2, Q=1 !"a<1" & !"b>2" & !dead 16->20 21 a=2, b=3, Q=1 !"a<1" & "b>2" & !dead 17->21 18->12 18->20 18->21 19->19 20->16 21->17

If we have an LTL proposition to check, we can convert it into an automaton using spot.translate(), and synchronize that automaton with the Kripke structure using spot.otf_product(). This otf_product() function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm "consumes" it (here the display routine).

In [12]:
a = spot.translate('"a<1" U "b>2"'); a
Out[12]:
[Büchi] 1 1 I->1 1->1 "a<1" & !"b>2" 0 0 1->0 "b>2" 0->0 1
In [13]:
spot.otf_product(k, a)
Out[13]:
Inf( ) [Büchi] 0 a=0, b=0, Q=0 * 1 I->0 1 a=1, b=0, Q=0 * 1 0->1 "a<1" & !"b>2" & !dead 2 a=0, b=1, Q=0 * 1 0->2 "a<1" & !"b>2" & !dead 3 a=1, b=1, Q=0 * 1 2->3 "a<1" & !"b>2" & !dead 4 a=0, b=2, Q=0 * 1 2->4 "a<1" & !"b>2" & !dead 5 a=1, b=2, Q=0 * 1 4->5 "a<1" & !"b>2" & !dead 6 a=0, b=3, Q=0 * 1 4->6 "a<1" & !"b>2" & !dead 7 a=0, b=2, Q=1 * 1 4->7 "a<1" & !"b>2" & !dead 8 a=0, b=3, Q=1 * 0 6->8 "a<1" & "b>2" & !dead u7 ... 7->u7 9 a=1, b=2, Q=1 * 1 7->9 "a<1" & !"b>2" & !dead 8->8 "a<1" & "b>2" & dead

If we want to create a model_check function that takes a model and formula, we need to get the list of atomic propositions used in the formula using atomic_prop_collect(). This returns an atomic_prop_set:

In [14]:
a = spot.atomic_prop_collect(spot.formula('"a < 2" W "b == 1"')); a
Out[14]:
$\{\unicode{x201C}\mathit{a < 2}\unicode{x201D}, \unicode{x201C}\mathit{b == 1}\unicode{x201D}\}$
In [15]:
def model_check(f, m):
    nf = spot.formula.Not(f)
    ss = m.kripke(spot.atomic_prop_collect(nf))
    return spot.otf_product(ss, nf.translate()).is_empty() 
In [16]:
model_check('"a<1" R "b > 1"', m)
Out[16]:
False

Instead of otf_product(x, y).is_empty() we prefer to call !x.intersects(y). There is also x.intersecting_run(y) that can be used to return a counterexample.

In [17]:
def model_debug(f, m):
    nf = spot.formula.Not(f)
    ss = m.kripke(spot.atomic_prop_collect(nf))
    return ss.intersecting_run(nf.translate())
In [19]:
run = model_debug('"a<1" R "b > 1"', m); print(run)
Prefix:
  a=0, b=0, Q=0
  |  "a<1" & !"b > 1" & !dead
  a=1, b=0, Q=0
  |  !"a<1" & !"b > 1" & !dead
  a=2, b=0, Q=0
  |  !"a<1" & !"b > 1" & !dead
Cycle:
  a=3, b=0, Q=0
  |  !"a<1" & !"b > 1" & dead

This accepting run can be represented as an automaton (the True argument requires the state names to be preserved). This can be more readable.

In [20]:
run.as_twa(True)
Out[20]:
t [all] 0 a=0, b=0, Q=0 I->0 1 a=1, b=0, Q=0 0->1 "a<1" & !"b > 1" & !dead 2 a=2, b=0, Q=0 1->2 !"a<1" & !"b > 1" & !dead 3 a=3, b=0, Q=0 2->3 !"a<1" & !"b > 1" & !dead 3->3 !"a<1" & !"b > 1" & dead
In [ ]: