Using Spot for teaching LTL and ω-automata (TEAL'26 demo)¶

https://spot.lre.epita.fr/

Quick intro¶

Spot is a C++ library for linear-time temporal logic and ω-automata.

It also comes with command-line tools, and Python bindings.

The latter allow notebooks such as this one, which can be easily used for research, prototyping, demonstration, teaching. In particular the notebook interface makes it easy to design lab sessions where students combine existing algorithms to build practical applications.

In addition to the above, the Spot website also has a web-based tool focused on LTL formulas and their mapping to ω-automata.

In [1]:
import spot
from spot.jupyter import display_inline
from copy import copy
spot.setup()

Simple objects: LTL, Büchi automata, words¶

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]:
f.translate()
Out[3]:
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 a 2 2 1->2 !a & b 2->2 b
In [4]:
a = spot.translate("a & !b & X!b & G(a <-> X!a) & G(b <-> XXX!b) & GFc")
a
Out[4]:
Inf( ⓿ ) [Büchi] 0 0 I->0 1 1 0->1 a & !b 2 2 1->2 !a & !b 3 3 2->3 a & !b 4 4 2->4 a & b 5 5 3->5 !a & b & !c 3->5 !a & b & c ⓿ 6 6 4->6 !a & b & !c 4->6 !a & b & c ⓿ 7 7 5->7 a & b & !c 5->7 a & b & c ⓿ 8 8 6->8 a & b & !c 6->8 a & b & c ⓿ 9 9 7->9 !a & b & !c 7->9 !a & b & c ⓿ 10 10 8->10 !a & !b & !c 8->10 !a & !b & c ⓿ 11 11 9->11 a & !b & !c 9->11 a & !b & c ⓿ 12 12 10->12 a & !b & !c 10->12 a & !b & c ⓿ 13 13 11->13 !a & !b & !c 11->13 !a & !b & c ⓿ 14 14 12->14 !a & !b & !c 12->14 !a & !b & c ⓿ 13->3 a & !b & !c 13->3 a & !b & c ⓿ 14->4 a & b & !c 14->4 a & b & c ⓿
In [5]:
r = a.accepting_run()
r.highlight(5)
a
Out[5]:
Inf( ⓿ ) [Büchi] 0 0 I->0 1 1 0->1 a & !b 2 2 1->2 !a & !b 3 3 2->3 a & !b 4 4 2->4 a & b 5 5 3->5 !a & b & !c 3->5 !a & b & c ⓿ 6 6 4->6 !a & b & !c 4->6 !a & b & c ⓿ 7 7 5->7 a & b & !c 5->7 a & b & c ⓿ 8 8 6->8 a & b & !c 6->8 a & b & c ⓿ 9 9 7->9 !a & b & !c 7->9 !a & b & c ⓿ 10 10 8->10 !a & !b & !c 8->10 !a & !b & c ⓿ 11 11 9->11 a & !b & !c 9->11 a & !b & c ⓿ 12 12 10->12 a & !b & !c 10->12 a & !b & c ⓿ 13 13 11->13 !a & !b & !c 11->13 !a & !b & c ⓿ 14 14 12->14 !a & !b & !c 12->14 !a & !b & c ⓿ 13->3 a & !b & !c 13->3 a & !b & c ⓿ 14->4 a & b & !c 14->4 a & b & c ⓿
In [6]:
w = spot.twa_word(r)
w
Out[6]:
$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 [7]:
w.show()
Out[7]:
abcprefixcycle cycle
In [8]:
w.use_all_aps(a.ap_vars())
w.show()
Out[8]:
abcprefixcycle cycle

Testing if two formulas are equivalent¶

In [9]:
f = spot.formula("a W (b R c)")
display(f)
g = f.unabbreviate("WR")
display(g)
$a \mathbin{\mathsf{W}} (b \mathbin{\mathsf{R}} c)$
$a \mathbin{\mathsf{U}} ((c \mathbin{\mathsf{U}} ((b \land c) \lor \mathsf{G} c)) \lor \mathsf{G} a)$
In [10]:
spot.are_equivalent(f, g)
Out[10]:
True

Enumerating words¶

In [11]:
ag = spot.translate('!a U (b & G(a <-> Xc))')
ag
Out[11]:
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
In [12]:
le = spot.lasso_enumerator(ag, min_stem=0, max_stem=2, min_cycle=1, max_cycle=2) 
while w := le.next_word():
    print(w)

!a & b; cycle{!a & !c}
a & b; cycle{a & c}
!a & b; cycle{!a & !c; !a & !c}
!a & b; cycle{a & !c; !a & c}
a & b; cycle{!a & c; a & !c}
a & b; cycle{a & c; a & c}
!a; !a & b; cycle{!a & !c}
!a; a & b; cycle{a & c}
!a & b; !a & !c; cycle{!a & !c}
!a & b; a & !c; cycle{a & c}
a & b; !a & c; cycle{!a & !c}
a & b; a & c; cycle{a & c}
!a; !a & b; cycle{!a & !c; !a & !c}
!a; !a & b; cycle{a & !c; !a & c}
!a; a & b; cycle{!a & c; a & !c}
!a; a & b; cycle{a & c; a & c}
!a & b; !a & !c; cycle{!a & !c; !a & !c}
!a & b; !a & !c; cycle{a & !c; !a & c}
!a & b; a & !c; cycle{!a & c; a & !c}
!a & b; a & !c; cycle{a & c; a & c}
a & b; !a & c; cycle{!a & !c; !a & !c}
a & b; !a & c; cycle{a & !c; !a & c}
a & b; a & c; cycle{!a & c; a & !c}
a & b; a & c; cycle{a & c; a & c}
In [13]:
le = spot.lasso_enumerator(ag, min_stem=0, max_stem=2, min_cycle=1, max_cycle=2) 
results=[]
while r := le.next_run():
    r.highlight(5)
    results.append(copy(ag))
    ag.remove_highlight_edges()
display_inline(*results, per_row=5)
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c

Example task: testing stutter-invariance, and returning counterexamples¶

A formula $\varphi$ is stutter-invariant iff $(w_1 \models \varphi) \iff (w_2 \models \varphi)$ for any pair of ω-words $(w_1,w_2)$ that differ only by removing duplicate letters, or by duplicating letters.

(Any $\mathsf{X}$-free LTL formula is necessarily stutter-invariant, but this is only a sufficient condition.)

In [14]:
f = spot.formula("F(a & X(!a & Gb))")
spot.is_stutter_invariant(f)
Out[14]:
True
In [15]:
g = spot.formula('!a U (b & G(a <-> Xc))')
spot.is_stutter_invariant(g)
Out[15]:
False

Let's find a proof for the stutter-sensitivity of g.

First, here is the closure operator, that allows automata to skip duplicate letters.

In [16]:
pos = g.translate()
In [17]:
display_inline(pos.show('.t'), spot.closure(pos), per_row=2)
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c ⓿ 1->2 a & !c ⓿ 2->1 !a & c ⓿ 2->2 a & c ⓿
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 0->1 !a & b & !c ⓿ 2 2 0->2 a & b 0->2 a & b & c ⓿ 1->1 !a & !c ⓿ 1->2 a & !c ⓿ 2->1 !a & c ⓿ 2->2 a & c ⓿

Using closure, we can build a stutter-invariance test using the following Theorem:

A formula $\varphi$ is stutter invariant iff $\mathcal{L}(closure(A_\varphi)) \cap \mathcal{L}(closure(A_{\lnot\varphi})) = \emptyset$

In [18]:
def is_stutter_invariant(g):
    pos = spot.formula(g).translate()
    neg = spot.formula.Not(g).translate()
    word = spot.product(spot.closure(pos),
                        spot.closure(neg)).accepting_word()
    if word is None:
        print(f"{g} is stutter-invariant")
        return
    print(f"{g} is not stutter-invariant")
    word.use_all_aps(pos.ap_vars())
    waut = word.as_automaton()
    if waut.intersects(pos):
        word2 = spot.sl2(waut).intersecting_word(neg)
        word2.simplify()
        accword, rejword = word, word2
    else:
        word2 = spot.sl2(waut).intersecting_word(pos)
        word2.simplify()
        accword, rejword = word2, word
    print(f"Accepted: {accword}\nRejected: {rejword}")
    pos.intersecting_run(accword.as_automaton()).highlight(4)
    display_inline(pos)
In [19]:
is_stutter_invariant(f)

F(a & X(!a & Gb)) is stutter-invariant
In [20]:
is_stutter_invariant(g)

!a U (b & G((a & Xc) | (!a & X!c))) is not stutter-invariant
Accepted: a & b & !c; !a & !b & c; cycle{!a & !b & !c}
Rejected: a & b & !c; a & b & !c; !a & !b & c; cycle{!a & !b & !c}
[Büchi] 0 0 I->0 0->0 !a 1 1 0->1 !a & b 2 2 0->2 a & b 1->1 !a & !c 1->2 a & !c 2->1 !a & c 2->2 a & c

Extensions to LTL: PSL and QLTL¶

Let's build an automaton that accepts all ω-words where $a$ holds at every even position. The "at every even position" part cannot be expressed in pure LTL without introducing an atomic proposition tracking even positions.

In [21]:
spot.translate('!even & G(even xor Xeven)')
Out[21]:
t [all] 1 1 I->1 0 0 1->0 !even 0->1 even
In [22]:
a = spot.translate('!even & G(even xor Xeven) & G(even -> a)')
a
Out[22]:
t [all] 0 0 I->0 1 1 0->1 !even 1->0 a & even
In [23]:
remover = spot.remove_ap()
remover.add_ap('even')
a = remover.strip(a)
a
Out[23]:
t [all] 0 0 I->0 1 1 0->1 1 1->0 a

Using Quantified-LTL, we can write the quantification inside the QLTL formula:

In [24]:
g = spot.formula('∃even: !even & G(even xor Xeven) & G(even -> a)')
In [25]:
g.translate()
Out[25]:
t [all] 0 0 I->0 1 1 0->1 1 1->0 a

Using PSL we can express this property without quantification.

The syntax $\{r\}\mathrel{\Box\kern-1.7pt\raise.4pt\hbox{$\mathord{\rightarrow}$}}\alpha$ means that $\alpha$ should hold on the infinite suffix starting on the last letter of any finite prefix matching $r$. So we just need $r$ to capture all finite words of even length.

In [26]:
h = spot.formula('{(1;1)*}[]->a')
In [27]:
h.translate()
Out[27]:
t [all] 0 0 I->0 1 1 0->1 1 1->0 a
In [28]:
spot.are_equivalent(g, h)
Out[28]:
True

Applications of LTL and ω-automata¶

Model Checking¶

Given a model $M$ and a formula $\varphi$, decide if $M\models \varphi$, i.e., $\mathcal{L}(M)\subseteq \mathcal{L}(\varphi)$.

In [29]:
import spot.ltsmin
In [30]:
%%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 tmpsd_0g30d.pml...
Parsing tmpsd_0g30d.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/tests/tmpsd_0g30d.pml.spins.c
Compiled C code to PINS library tmpsd_0g30d.pml.spins
In [31]:
model
Out[31]:
ltsmin model with the following variables:
  P_0._pc: pc
  P_0.a: int
  P_0.b: int
In [ ]:
k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k.show(".<5")
In [ ]:
k.show('.1K<5')

To test if $M \models \varphi$, we verify that $\mathcal{L}(M\otimes A_{\lnot\varphi})=\emptyset$.

In [ ]:
def model_check(M, φ):
    notφ = spot.formula.Not(φ)
    ss = M.kripke(spot.atomic_prop_collect(notφ))
    return spot.otf_product(ss, notφ.translate()).is_empty() #.accepting_run().project(ss).as_twa(True)
In [ ]:
model_check(model, 'F("P_0.b > 2")')

Reactive Synthesis¶

Given a partition of atomic propositions as inputs and output ($AP=\mathcal{I}\uplus\mathcal{O}$) decide if it is possible to build a reactive controller, that assigns values to output propositions based on the history of input values, in such a way that an LTL specification over both types of propositions is satisfied.

In [32]:
import buddy
In [33]:
spec = spot.formula("(F(i0 & X(i1)) <-> Fo)")
spec
Out[33]:
$\mathsf{F} (i_{0} \land \mathsf{X} i_{1}) \leftrightarrow \mathsf{F} o$
In [34]:
dpa = spec.translate('parity', 'det')  # in the general case, we want a DPA
dpa
Out[34]:
[Büchi] 0 0 I->0 0->0 !i0 & !o 1 1 0->1 !i0 & o 2 2 0->2 i0 & !o 3 3 0->3 i0 & o 1->1 !i0 1->3 i0 2->0 !i0 & !i1 & !o 2->1 !i0 & !i1 & o 2->2 i0 & !i1 & !o 2->3 i0 & !i1 & o 4 4 2->4 i1 & !o 5 5 2->5 i1 & o 3->1 !i0 & !i1 3->3 i0 & !i1 3->5 i1 4->4 !o 4->5 o 5->5 1
In [35]:
bddout = buddy.bdd_ithvar(dpa.register_ap('o'))
game = spot.split_2step(dpa, bddout)
game
Out[35]:
Inf( ⓿ ) [Büchi] 0 0 I->0 6 6 0->6 !i0 ⓿ 7 7 0->7 i0 ⓿ 6->0 !o ⓿ 1 1 6->1 o ⓿ 2 2 7->2 !o ⓿ 3 3 7->3 o ⓿ 8 8 1->8 !i0 9 9 1->9 i0 8->1 1 9->3 1 2->6 !i0 & !i1 ⓿ 2->7 i0 & !i1 ⓿ 10 10 2->10 i1 ⓿ 4 4 10->4 !o ⓿ 5 5 10->5 o ⓿ 3->8 !i0 & !i1 3->9 i0 & !i1 11 11 3->11 i1 11->5 1 12 12 4->12 1 12->4 !o 12->5 o 13 13 5->13 1 ⓿ 13->5 1 ⓿
In [36]:
spot.solve_game(game)
Out[36]:
True
In [37]:
spot.highlight_strategy(game)
game
Out[37]:
Inf( ⓿ ) [Büchi] 0 0 I->0 6 6 0->6 !i0 ⓿ 7 7 0->7 i0 ⓿ 6->0 !o ⓿ 1 1 6->1 o ⓿ 2 2 7->2 !o ⓿ 3 3 7->3 o ⓿ 8 8 1->8 !i0 9 9 1->9 i0 8->1 1 9->3 1 2->6 !i0 & !i1 ⓿ 2->7 i0 & !i1 ⓿ 10 10 2->10 i1 ⓿ 4 4 10->4 !o ⓿ 5 5 10->5 o ⓿ 3->8 !i0 & !i1 3->9 i0 & !i1 11 11 3->11 i1 11->5 1 12 12 4->12 1 12->4 !o 12->5 o 13 13 5->13 1 ⓿ 13->5 1 ⓿
In [38]:
m = spot.solved_game_to_separated_mealy(game)
m
Out[38]:
0 0 I->0 0->0 !i0 / !o 1 1 0->1 i0 / !o 1->0 !i0 & !i1 / !o 1->1 i0 & !i1 / !o 2 2 1->2 i1 / !o 3 3 2->3 1 / o 3->3 1 / 1
In [39]:
spot.reduce_mealy_here(m)
m
Out[39]:
0 0 I->0 0->0 !i0 / !o 1 1 0->1 i0 / !o 1->0 !i0 & !i1 / !o 1->1 i0 & !i1 / !o 2 2 1->2 i1 / !o 2->1 1 / o
In [40]:
spot.mealy_machine_to_aig(m, "isop").show("h")
Out[40]:
6 L0_out 10 10 6->10 12 12 6->12 22 22 6->22 8 L1_out 8->10 16 16 8->16 24 24 8->24 18 18 10->18 o0 o 10->o0:w 12->18 14 14 14->16 20 20 16->20 18->20 L0 L0_in 20->L0 22->24 L1 L1_in 24->L1 2 i1 2->14 2->22 4 i0 4->12 4->14

Interactive visualisations¶

In [ ]:
a = spot.automaton('colorful2.hoa')
a
In [ ]:
spot.acd(a)

Protyping with graphical logs¶

In [ ]:
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 [ ]:
log_is_empty1("", a)

Running other tools and explaining their output¶

In [ ]:
def ltl2dela(f):
    f = spot.formula(f)
    return spot.automaton(f"owl ltl2dela -f {f:q} |")
In [ ]:
f = "(a U b) & (GFa -> FGb)"
aut = ltl2dela(f)
aut
In [ ]:
spot.match_states_decorate(aut, f)
aut
In [ ]: