

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]:



In [10]:

    
k.show('.<15')









    Out[10]:



In [11]:

    
k.show('.<0')  # unlimited output









    Out[11]:



In [12]:

    
a = spot.translate('"a<1" U "b>2"'); a









    Out[12]:



In [13]:

    
spot.otf_product(k, a)









    Out[13]:

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]:





$\{``\mathit{a < 2}\textrm{''}, ``\mathit{b == 1}\textrm{''}\}$



In [15]:

    
def model_check(f, m):
    f = spot.formula(f)
    ss = m.kripke(spot.atomic_prop_collect(f))
    nf = spot.formula_Not(f).translate()
    return spot.otf_product(ss, nf).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 [21]:

    
def model_debug(f, m):
    f = spot.formula(f)
    ss = m.kripke(spot.atomic_prop_collect(f))
    nf = spot.formula_Not(f).translate()
    return ss.intersecting_run(nf)



In [23]:

    
run = model_debug('"a<1" R "b > 1"', m); run









    Out[23]:





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 [24]:

    
run.as_twa(True)









    Out[24]: