In [1]:
import spot
import spot.ltsmin
spot.setup()
Part 3 – Python bindings with visualizations¶
Simple objects: LTL, automata¶
In [2]:
f = spot.formula("F(a & X(!a & Gb))")
f
Out[2]:
$\mathsf{F} (a \land \mathsf{X} (\lnot a \land \mathsf{G} b))$
In [3]:
aut = spot.translate(f)
aut
Out[3]:
In [4]:
spot.is_stutter_invariant(f)
Out[4]:
True
In [5]:
a = spot.translate("a & !b & X!b & G(a <-> X!a) & G(b <-> XXX!b) & GFc")
a
Out[5]:
In [6]:
r = a.accepting_run()
r.highlight(5)
a
Out[6]:
In [7]:
w = spot.twa_word(r)
w
Out[7]:
$a \land \lnot b; \lnot a \land \lnot b; a \land \lnot b; \mathsf{cycle}\{\lnot a \land b \land c; a \land b \land \lnot c; \lnot a \land b \land \lnot c; a \land \lnot b \land \lnot c; \lnot a \land \lnot b \land \lnot c; a \land \lnot b \land \lnot c\}$
In [8]:
w.show()
Out[8]:
In [9]:
a = spot.automaton("colorful2.hoa")
a
Out[9]:
In [10]:
r = a.accepting_run()
r.highlight(5)
a
Out[10]:
Model Checking with the LTSmin interface¶
In [11]:
%%pml model
active proctype P() {
int a = 0;
int b = 0;
x: if
:: a < 3 && b < 3 -> a = a + 1; goto x;
:: 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 tmp51y3jmi6.pml... Parsing tmp51y3jmi6.pml done (0.0 sec) Optimizing graphs... StateMerging changed 2 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-grow/jupyter/tmp51y3jmi6.pml.spins.c Compiled C code to PINS library tmp51y3jmi6.pml.spins
In [12]:
model
Out[12]:
ltsmin model with the following variables: P_0._pc: pc P_0.a: int P_0.b: int
In [13]:
k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k.show(".<5")
Out[13]:
In [14]:
k.show('.1K<5')
Out[14]:
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() #.accepting_run().project(ss).as_twa(True)
In [16]:
model_check('F("P_0.b > 2")', model)
Out[16]:
False
SAT-based Minimization¶
In [17]:
def ltl2dstar(f):
f = spot.formula(f)
return spot.automaton(f"echo {f:lq} | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |")
In [18]:
a = ltl2dstar("(FGa | Fb) & FGc")
a
Out[18]:
In [19]:
spot.sat_minimize(a)
Out[19]:
In [20]:
spot.sat_minimize(a, state_based=True)
Out[20]:
In [21]:
spot.sat_minimize(a, acc="Rabin 1", display_log=True)
| input.states | target.states | reachable.states | edges | transitions | variables | clauses | enc.user | enc.sys | sat.user | sat.sys | |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 5 | 3 | 3 | 10 | 24 | 810 | 25262 | 1 | 0 | 0 | 0 |
| 1 | 3 | 1 | NaN | NaN | NaN | 69 | 676 | 0 | 0 | 0 | 0 |
| 2 | 3 | 2 | 2 | 6 | 16 | 276 | 5299 | 0 | 0 | 0 | 0 |
Out[21]:
ACD with Interactive visualization¶
ACD = Alternative Cycle Decomposition
In [22]:
a = spot.automaton("colorful2.hoa")
acd = spot.acd(a)
acd
Out[22]:
In [23]:
spot.acd_transform(a) # this converts into a Parity automaton
Out[23]:
Prototyping with graphical logs...¶
In [24]:
def print_scc_info(si, log=""):
n = si.scc_count()
print(log, "Number of SCCs:", n)
for s in range(n):
print("{} - SCC{}: {}{}".format(log, s, si.states_of(s), " trivial" if si.is_trivial(s) else ""))
def display_scc(si, sccnum):
display(si.split_on_sets(sccnum, [], True)[0])
def log_is_empty1(log, g):
print(log, "is_empty() running SCC decomposition")
# We need to pass the TRACK_STATE option for print_scc_info() to work
si = spot.scc_info_with_options(g, spot.scc_info_options_TRACK_STATES)
print_scc_info(si, log)
for scc_num in range(si.scc_count()):
if si.is_trivial(scc_num):
continue
if not log_is_scc_empty1("{}SCC{}:".format(log, scc_num), si, scc_num):
return False
return True
def log_is_scc_empty1(log, si, scc_num, acc=None):
if acc is None:
acc = si.get_aut().acc()
print("{} is_scc_empty() on".format(log))
display_scc(si, scc_num)
occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num)
print("{} occur={}, common={}".format(log, occur, common))
acc = acc.restrict_to(occur)
acc = acc.remove(common, False)
print("{} acceptance reduced to {}".format(log, acc.get_acceptance()))
if acc.is_t(): return False
if acc.is_f(): return True
if acc.accepting(occur): return False
for idx, cl in enumerate(acc.top_disjuncts()):
print("{}clause{}: checking clause {}".format(log, idx, cl.get_acceptance()))
fu = cl.fin_unit() # Is there Fin at the top level
if fu:
print("{}clause{}: unit-Fin(s) present {}".format(log, idx, fu))
with spot.scc_and_mark_filter(si, scc_num, fu) as filt:
filt.override_acceptance(cl.remove(fu, True))
if not log_is_empty1("{}clause{}:Fin{}=1:".format(log, idx, fu), filt):
return False
else:
# Pick some Fin term anywhere in the formula
fo = cl.fin_one()
print("{}clause{}: arbritrary Fin selected {}".format(log, idx, fo))
# Try to solve assuming Fin(fo)=True
with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt:
filt.override_acceptance(cl.remove([fo], True))
if not log_is_empty1("{}clause{}:Fin({})=1:".format(log, idx, fo), filt):
return False
# Try to solve assuming Fin(fo)=False
if not log_is_scc_empty1("{}clause{}:Fin({})=0:".format(log, idx, fo),
si, scc_num, acc.force_inf([fo])):
return False
return True
In [25]:
log_is_empty1("", a)
is_empty() running SCC decomposition Number of SCCs: 2 - SCC0: (1, 4, 2, 6, 5) - SCC1: (0, 3) SCC0: is_scc_empty() on
SCC0: occur={1,2,3,4,5}, common={}
SCC0: acceptance reduced to Fin(1) | ((Fin(4)|Fin(5)) & (Inf(2)&Inf(3)))
SCC0:clause0: checking clause Fin(1)
SCC0:clause0: unit-Fin(s) present {1}
SCC0:clause0:Fin{1}=1: is_empty() running SCC decomposition
SCC0:clause0:Fin{1}=1: Number of SCCs: 3
SCC0:clause0:Fin{1}=1: - SCC0: (1, 4, 2)
SCC0:clause0:Fin{1}=1: - SCC1: (6,) trivial
SCC0:clause0:Fin{1}=1: - SCC2: (5,) trivial
SCC0:clause0:Fin{1}=1:SCC0: is_scc_empty() on
SCC0:clause0:Fin{1}=1:SCC0: occur={2,4,5}, common={4}
SCC0:clause0:Fin{1}=1:SCC0: acceptance reduced to t
Out[25]:
False
Part 4 – Reactive synthesis¶
LTL synthesis¶
In [26]:
spec = spot.formula("(F(i0 & X(i1)) <-> Fo)")
spec
Out[26]:
$\mathsf{F} (i_{0} \land \mathsf{X} i_{1}) \leftrightarrow \mathsf{F} o$
In [27]:
game = spot.automaton(f"ltlsynt -f {spec:q} --decompose=no --print-game|")
game.show('.t')
Out[27]:
In [28]:
spot.solve_game(game)
Out[28]:
True
In [29]:
spot.highlight_strategy(game)
game.show(".t")
Out[29]:
In [30]:
m = spot.solved_game_to_separated_mealy(game)
m
Out[30]:
In [31]:
spot.reduce_mealy_here(m)
m
Out[31]:
In [32]:
spot.mealy_machine_to_aig(m, "isop").show("h")
Out[32]:
LTLf Synthesis?¶
In [33]:
spec_ltlf = spot.formula("(F(i0 & Xi1) <-> GFo) && X[!]1")
spec_ltlf
Out[33]:
$(\mathsf{F} (i_{0} \land \mathsf{X} i_{1}) \leftrightarrow \mathsf{G} \mathsf{F} o) \land \mathsf{X^{[!]}}\top$
LTLf translation Via LTL?¶
In [34]:
spec_ltl = spot.from_ltlf(spec_ltlf)
spec_ltl
Out[34]:
$\mathit{alive} \land (\mathsf{F} (\mathit{alive} \land i_{0} \land \mathsf{X} (\lnot \mathit{alive} \lor i_{1})) \leftrightarrow \mathsf{G} (\lnot \mathit{alive} \lor \mathsf{F} (\mathit{alive} \land o))) \land \mathsf{X} \mathit{alive} \land (\mathit{alive} \mathbin{\mathsf{U}} \mathsf{G} \lnot \mathit{alive})$
In [35]:
dba = spot.translate(spec_ltl, "det")
dba
Out[35]:
In [36]:
dfa = spot.to_finite(dba)
dfa
Out[36]:
Using MONA-like MTBDD-based DFA¶
This stuff is not yet released, at the time of Spin'25. It will be part of Spot 2.14.
In [37]:
mtdfa = spot.ltlf_to_mtdfa(spec_ltlf)
mtdfa
Out[37]:
In [38]:
mtdfa.as_twa()
Out[38]:
In [39]:
spot.product_xor(spot.twadfa_to_mtdfa(dfa), mtdfa).is_empty()
Out[39]:
True
In [40]:
with spot.bdd_dict_preorder("i1", "i0") as d:
a = spot.ltlf_to_mtdfa(spec_ltlf, dict=d)
a.set_controllable_variables("o")
In [41]:
a
Out[41]:
In [42]:
with spot.bdd_dict_preorder("i1", "i0") as d:
a = spot.ltlf_to_mtdfa_for_synthesis(spec_ltlf, ["o"], dict=d)
a
Out[42]:
In [43]:
m = spot.mtdfa_strategy_to_mealy(a)
m
Out[43]:
In [44]:
spot.reduce_mealy_here(m)
m
Out[44]:
In [45]:
spot.mealy_machine_to_aig(m, "isop").show("h")
Out[45]:
In [ ]: