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]:
b'\n\n\n\n\n\n0\n\nc=1, x1=0, x2=0, a1=0, a2=0\na1.Q & !"c==17" & !dead\n\n\n\nI->0\n\n\n\n\n\n1\n\nc=1, x1=1, x2=0, a1=1, a2=0\n!a1.Q & !"c==17" & !dead\n\n\n\n0->1\n\n\n\n\n\n2\n\nc=1, x1=0, x2=1, a1=0, a2=1\na1.Q & !"c==17" & !dead\n\n\n\n0->2\n\n\n\n\n\n3\n\nc=1, x1=2, x2=0, a1=2, a2=0\n!a1.Q & !"c==17" & !dead\n\n\n\n1->3\n\n\n\n\n\n4\n\nc=1, x1=1, x2=1, a1=1, a2=1\n!a1.Q & !"c==17" & !dead\n\n\n\n1->4\n\n\n\n\n\n2->4\n\n\n\n\n\n5\n\nc=1, x1=0, x2=2, a1=0, a2=2\na1.Q & !"c==17" & !dead\n\n\n\n2->5\n\n\n\n\n\n6\n\nc=2, x1=2, x2=0, a1=0, a2=0\n...\n\n\n\n3->6\n\n\n\n\n\n7\n\nc=1, x1=2, x2=1, a1=2, a2=1\n...\n\n\n\n3->7\n\n\n\n\n\n4->7\n\n\n\n\n\n8\n\nc=1, x1=1, x2=2, a1=1, a2=2\n...\n\n\n\n4->8\n\n\n\n\n\n5->8\n\n\n\n\n\n9\n\nc=2, x1=0, x2=2, a1=0, a2=0\n...\n\n\n\n5->9\n\n\n\n\n\nu6\n\n\n...\n\n\n\n\n\n6->u6\n\n\n\n\n\n\n\n\nu7\n\n\n...\n\n\n\n\n\n7->u7\n\n\n\n\n\n\n\n\nu8\n\n\n...\n\n\n\n\n\n8->u8\n\n\n\n\n\n\n\n\nu9\n\n\n...\n\n\n\n\n\n9->u9\n\n\n\n\n\n\n\n\n'
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