In [1]:
from IPython.display import display, HTML
import spot
spot.setup()

To translate a formula into a Testing Automaton

Start by building a Büchi automaton

In [2]:
f = spot.formula('a U Gb')
a = f.translate('ba')
a
Out[2]:
[Büchi] 0 0 I->0 0->0 a 1 1 0->1 b 1->1 b

Then, gather all the atomic proposition in the formula, and create an automaton with changesets

In [3]:
propset = spot.atomic_prop_collect_as_bdd(f, a)
ta = spot.tgba_to_ta(a, propset, True, True, False, False, True)
ta.show('.A')
Out[3]:
G 1 init 0->1 2 0 !a & b 1->2 !a & b 3 0 a & !b 1->3 a & !b 4 0 a & b 1->4 a & b 5 1 !a & !b 2->5 {b} 6 1 !a & b 2->6 {} 7 1 a & !b 2->7 {a, b} 8 1 a & b 2->8 {a} 3->2 {a, b} 3->3 {} 3->4 {b} 9 0 !a & !b 3->9 {a} 4->2 {a} 4->3 {b} 4->4 {} 4->5 {a, b} 4->6 {a} 4->7 {b} 4->8 {} 4->9 {a, b} 6->5 {b} 6->6 {} 6->7 {a, b} 6->8 {a} 8->5 {a, b} 8->6 {a} 8->7 {b} 8->8 {}

Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by {}), marking as livelock accepting (rectangles) any states from which there exists a an accepting path labeled by {}.

In [4]:
ta = spot.tgba_to_ta(a, propset, True, True, False, False, False)
ta.show('.A')
Out[4]:
G 1 init 0->1 2 0 !a & b 1->2 !a & b 3 0 a & !b 1->3 a & !b 4 0 a & b 1->4 a & b 5 1 a & b 2->5 {a} 3->2 {a, b} 3->4 {b} 4->2 {a} 4->3 {b} 6 1 !a & b 4->6 {a} 5->6 {a} 6->5 {a}

Finally, use bisimulation to minimize the number of states.

In [5]:
spot.minimize_ta(ta).show('.A')
Out[5]:
G 1 init 0->1 2 2 1->2 !a & b 3 1 1->3 a & !b 4 3 1->4 a & b 5 4 2->5 {a} 3->2 {a, b} 3->4 {b} 4->2 {a} 4->3 {b} 4->5 {a} 5->5 {a}