a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a

"""
Explanation: 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).
End of explanation
"""


a.show("v")

"""
Explanation: 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.
End of explanation
"""


a.show(".ast")

"""
Explanation: 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:
End of explanation
"""


f = spot.formula('a U b'); f

spot.translate(f)

f.translate()

"""
Explanation: The translate() function can also be called with a formula object.  Either as a function, or as a method.
End of explanation
"""


f.translate('mon')

"""
Explanation: When used as a method, all the arguments are translation options.  Here is a monitor:
End of explanation
"""


f = spot.formula('Ga | Gb | Gc'); f

f.translate('ba', 'small').show('.v')

f.translate('ba', 'det').show('v.')

"""
Explanation: The following three cells show a formulas for which it makes a difference to select 'small' or 'deterministic'.
End of explanation
"""


spot.translate('GFa -> GFb', 'unambig')

"""
Explanation: Here is how to build an unambiguous automaton:
End of explanation
"""


spot.translate('GFa -> GFb')

"""
Explanation: Compare with the standard translation:
End of explanation
"""


spot.translate('GFa -> GFb', 'sbacc')

"""
Explanation: And here is the automaton above with state-based acceptance:
End of explanation
"""


a = spot.translate('F(a & X(!a &Xb))', "any"); a

spot.sl(a)

a.is_empty()

"""
Explanation: Some example of running the self-loopization algorithm on an automaton:
End of explanation
"""


%%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--

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'))

!rm example1.aut

spot.complete(a)

spot.complete(spot.translate('Ga'))

# 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'))

"""
Explanation: Reading from file (see automaton-io.ipynb for more examples).
End of explanation
"""


a = spot.translate('FGa')
display(a)
display(a.is_deterministic())

spot.tgba_determinize(a).show('.ba')

"""
Explanation: Explicit determinization after translation:
End of explanation
"""


aut = spot.translate('FGa', 'generic', 'deterministic'); aut

"""
Explanation: Determinization by translate().  The generic option allows any acceptance condition to be used instead of the default generalized Büchi.
End of explanation
"""


import buddy
b = buddy.bdd_ithvar(aut.register_ap('b'))
for e in aut.edges():
    e.cond &= b
aut

"""
Explanation: Adding an automatic proposition to all edges
End of explanation
"""


c = buddy.bdd_ithvar(aut.register_ap('c'))
for e in aut.out(0):
    if e.dst == 1:
        e.cond &= c
aut

"""
Explanation: Adding an atomic proposition to the edge between 0 and 1:
End of explanation
"""


