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'\n\n\n[B\xc3\xbcchi]\n\n\n\n0\n\n0\n\n\n\nI->0\n\n\n\n\n\n0->0\n\n\na\n\n\n\n1\n\n\n1\n\n\n\n0->1\n\n\nb\n\n\n\n1->1\n\n\nb\n\n\n\n'

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]:
b'\n\nG\n\n\n\n\n1\n\ninit\n\n\n\n0->1\n\n\n\n\n\n2\n\n0\n!a & b\n\n\n\n1->2\n\n\n!a & b\n\n\n\n3\n\n0\na & !b\n\n\n\n1->3\n\n\na & !b\n\n\n\n4\n\n0\na & b\n\n\n\n1->4\n\n\na & b\n\n\n\n5\n\n\n1\n!a & !b\n\n\n\n2->5\n\n\n{b}\n\n\n\n6\n\n\n1\n!a & b\n\n\n\n2->6\n\n\n{}\n\n\n\n7\n\n\n1\na & !b\n\n\n\n2->7\n\n\n{a, b}\n\n\n\n8\n\n\n1\na & b\n\n\n\n2->8\n\n\n{a}\n\n\n\n3->2\n\n\n{a, b}\n\n\n\n3->3\n\n\n{}\n\n\n\n3->4\n\n\n{b}\n\n\n\n9\n\n0\n!a & !b\n\n\n\n3->9\n\n\n{a}\n\n\n\n4->2\n\n\n{a}\n\n\n\n4->3\n\n\n{b}\n\n\n\n4->4\n\n\n{}\n\n\n\n4->5\n\n\n{a, b}\n\n\n\n4->6\n\n\n{a}\n\n\n\n4->7\n\n\n{b}\n\n\n\n4->8\n\n\n{}\n\n\n\n4->9\n\n\n{a, b}\n\n\n\n6->5\n\n\n{b}\n\n\n\n6->6\n\n\n{}\n\n\n\n6->7\n\n\n{a, b}\n\n\n\n6->8\n\n\n{a}\n\n\n\n8->5\n\n\n{a, b}\n\n\n\n8->6\n\n\n{a}\n\n\n\n8->7\n\n\n{b}\n\n\n\n8->8\n\n\n{}\n\n\n\n'

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]:
b'\n\nG\n\n\n\n\n1\n\ninit\n\n\n\n0->1\n\n\n\n\n\n2\n\n0\n!a & b\n\n\n\n1->2\n\n\n!a & b\n\n\n\n3\n\n0\na & !b\n\n\n\n1->3\n\n\na & !b\n\n\n\n4\n\n0\na & b\n\n\n\n1->4\n\n\na & b\n\n\n\n5\n\n\n1\na & b\n\n\n\n2->5\n\n\n{a}\n\n\n\n3->2\n\n\n{a, b}\n\n\n\n3->4\n\n\n{b}\n\n\n\n4->2\n\n\n{a}\n\n\n\n4->3\n\n\n{b}\n\n\n\n6\n\n\n1\n!a & b\n\n\n\n4->6\n\n\n{a}\n\n\n\n5->6\n\n\n{a}\n\n\n\n6->5\n\n\n{a}\n\n\n\n'

Finally, use bisimulation to minimize the number of states.

In [5]:
spot.minimize_ta(ta).show('.A')
Out[5]:
b'\n\nG\n\n\n\n\n1\n\ninit\n\n\n\n0->1\n\n\n\n\n\n2\n\n2\n\n\n\n1->2\n\n\n!a & b\n\n\n\n3\n\n1\n\n\n\n1->3\n\n\na & !b\n\n\n\n4\n\n3\n\n\n\n1->4\n\n\na & b\n\n\n\n5\n\n\n4\n\n\n\n2->5\n\n\n{a}\n\n\n\n3->2\n\n\n{a, b}\n\n\n\n3->4\n\n\n{b}\n\n\n\n4->2\n\n\n{a}\n\n\n\n4->3\n\n\n{b}\n\n\n\n4->5\n\n\n{a}\n\n\n\n5->5\n\n\n{a}\n\n\n\n'