This example is the right part of Fig.2 in our ATVA'16 paper titled "Spot 2.0 — a framework for LTL and ω-automata manipulation" slightly updated to benefit from improvements in more recent versions of Spot.

In [1]:
import spot
import spot.ltsmin
spot.setup(show_default='.Ab', max_states=10)
# This extra line ensures that our test suite skips this test if divine is not installed.
spot.ltsmin.require('divine')
In [2]:
%%dve adding
int c=1, x1, x2;
process a1 {
  state Q, R, S;  init Q;
  trans Q -> R { guard c<20; effect x1 = c; },
        R -> S { effect x1 = x1 + c; },
        S -> Q { effect c = x1; };
}
process a2 {
  state Q, R, S;  init Q;
  trans Q -> R { guard c<20; effect x2 = c; },
        R -> S { effect x2 = x2 + c; },
        S -> Q { effect c = x2; };
}
system async;
In [3]:
adding
Out[3]:
ltsmin model with the following variables:
  c: int
  x1: int
  x2: int
  a1: ['Q', 'R', 'S']
  a2: ['Q', 'R', 'S']
In [4]:
adding.kripke(['a1.Q', 'c==17'])
Out[4]:
0 c=1, x1=0, x2=0, a1=0, a2=0 a1.Q & !"c==17" & !dead I->0 1 c=1, x1=1, x2=0, a1=1, a2=0 !a1.Q & !"c==17" & !dead 0->1 2 c=1, x1=0, x2=1, a1=0, a2=1 a1.Q & !"c==17" & !dead 0->2 3 c=1, x1=2, x2=0, a1=2, a2=0 !a1.Q & !"c==17" & !dead 1->3 4 c=1, x1=1, x2=1, a1=1, a2=1 !a1.Q & !"c==17" & !dead 1->4 2->4 5 c=1, x1=0, x2=2, a1=0, a2=2 a1.Q & !"c==17" & !dead 2->5 6 c=2, x1=2, x2=0, a1=0, a2=0 ... 3->6 7 c=1, x1=2, x2=1, a1=2, a2=1 ... 3->7 4->7 8 c=1, x1=1, x2=2, a1=1, a2=2 ... 4->8 5->8 9 c=2, x1=0, x2=2, a1=0, a2=0 ... 5->9 u6 ... 6->u6 u7 ... 7->u7 u8 ... 8->u8 u9 ... 9->u9
In [5]:
def model_check(model, f):
    nf = spot.formula.Not(f)
    ss = model.kripke(spot.atomic_prop_collect(nf))
    return not ss.intersects(nf.translate())
In [6]:
model_check(adding, 'F("c==2")')
Out[6]:
True