In [1]:
from IPython.display import display
import spot
spot.setup()
To build an automaton, simply call translate() with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the ltl2tgba tool, and they can be abbreviated).
In [2]:
a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a
Out[2]:
The call the spot.setup() in the first cells has installed a default style for the graphviz output. If you want to change this style temporarily, you can call the show(style) method explicitely. For instance here is a vertical layout with the default font of GraphViz.
In [3]:
a.show("v")
Out[3]:
If you want to add some style options to the existing one, pass a dot to the show() function in addition to your own style options:
In [4]:
a.show(".ast")
Out[4]:
The translate() function can also be called with a formula object. Either as a function, or as a method.
In [5]:
f = spot.formula('a U b'); f
Out[5]:
In [6]:
spot.translate(f)
Out[6]:
In [7]:
f.translate()
Out[7]:
When used as a method, all the arguments are translation options. Here is a monitor:
In [8]:
f.translate('mon')
Out[8]:
The following three cells show a formulas for which it makes a difference to select 'small' or 'deterministic'.
In [9]:
f = spot.formula('Ga | Gb | Gc'); f
Out[9]:
In [10]:
f.translate('ba', 'small').show('.v')
Out[10]:
In [11]:
f.translate('ba', 'det').show('v.')
Out[11]:
Here is how to build an unambiguous automaton:
In [12]:
spot.translate('GFa -> GFb', 'unambig')
Out[12]:
Compare with the standard translation:
In [13]:
spot.translate('GFa -> GFb')
Out[13]:
And here is the automaton above with state-based acceptance:
In [14]:
spot.translate('GFa -> GFb', 'sbacc')
Out[14]:
Some example of running the self-loopization algorithm on an automaton:
In [15]:
a = spot.translate('F(a & X(!a &Xb))', "any"); a
Out[15]:
In [16]:
spot.sl(a)
Out[16]:
In [17]:
a.is_empty()
Out[17]:
Reading from file (see automaton-io.ipynb for more examples).
In [18]:
%%file example1.aut
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(1)
--BODY--
State: 0 {3}
[t] 0
[0] 1 {1}
[!0] 2 {0}
State: 1 {3}
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
--END--
In [19]:
a = spot.automaton('example1.aut')
display(a.show('.a'))
display(spot.remove_fin(a).show('.a'))
display(a.postprocess('TGBA', 'complete').show('.a'))
display(a.postprocess('BA'))
In [20]:
!rm example1.aut
In [21]:
spot.complete(a)
Out[21]:
In [22]:
spot.complete(spot.translate('Ga'))
Out[22]:
In [23]:
# Using +1 in the display options is a convient way to shift the
# set numbers in the output, as an aid in reading the product.
a1 = spot.translate('a W c'); display(a1.show('.bat'))
a2 = spot.translate('a U b'); display(a2.show('.bat+1'))
# the product should display pairs of states, unless asked not to (using 1).
p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))
Explicit determinization after translation:
In [24]:
a = spot.translate('FGa')
display(a)
display(a.is_deterministic())
In [25]:
spot.tgba_determinize(a).show('.ba')
Out[25]:
Determinization by translate(). The generic option allows any acceptance condition to be used instead of the default generalized Büchi.
In [26]:
aut = spot.translate('FGa', 'generic', 'deterministic'); aut.show('.ba')
Out[26]:
Translation to co-Büchi automaton
In [27]:
spot.translate('FGa', 'coBuchi').show('.ba')
Out[27]:
In [28]:
spot.translate('FGa', 'coBuchi', 'deterministic').show('.ba')
Out[28]:
Adding an atomic proposition to all edges
In [29]:
import buddy
b = buddy.bdd_ithvar(aut.register_ap('b'))
for e in aut.edges():
e.cond &= b
aut
Out[29]:
Adding an atomic proposition to the edge between 0 and 1:
In [30]:
c = buddy.bdd_ithvar(aut.register_ap('c'))
for e in aut.out(0):
if e.dst == 1:
e.cond &= c
aut
Out[30]: