<jupyter_start><jupyter_text>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).<jupyter_code>a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a<jupyter_output><empty_output><jupyter_text>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.<jupyter_code>a.show("v")<jupyter_output><empty_output><jupyter_text>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:<jupyter_code>a.show(".ast")<jupyter_output><empty_output><jupyter_text>The `translate()` function can also be called with a formula object.  Either as a function, or as a method.<jupyter_code>f = spot.formula('a U b'); f
spot.translate(f)
f.translate()<jupyter_output><empty_output><jupyter_text>When used as a method, all the arguments are translation options.  Here is a monitor:<jupyter_code>f.translate('mon')<jupyter_output><empty_output><jupyter_text>The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`.<jupyter_code>f = spot.formula('Ga | Gb | Gc'); f
f.translate('ba', 'small').show('.v')
f.translate('ba', 'det').show('v.')<jupyter_output><empty_output><jupyter_text>Here is how to build an unambiguous automaton:<jupyter_code>spot.translate('GFa -> GFb', 'unambig')<jupyter_output><empty_output><jupyter_text>Compare with the standard translation:<jupyter_code>spot.translate('GFa -> GFb')<jupyter_output><empty_output><jupyter_text>And here is the automaton above with state-based acceptance:<jupyter_code>spot.translate('GFa -> GFb', 'sbacc')<jupyter_output><empty_output><jupyter_text>Some example of running the self-loopization algorithm on an automaton:<jupyter_code>a = spot.translate('F(a & X(!a &Xb))', "any"); a
spot.sl(a)
a.is_empty()<jupyter_output><empty_output><jupyter_text>Reading from file (see `automaton-io.ipynb` for more examples).<jupyter_code>%%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'))<jupyter_output><empty_output><jupyter_text>Explicit determinization after translation:<jupyter_code>a = spot.translate('FGa')
display(a)
display(a.is_deterministic())
spot.tgba_determinize(a).show('.ba')<jupyter_output><empty_output><jupyter_text>Determinization by `translate()`.  The `generic` option allows any acceptance condition to be used instead of the default generalized Büchi.<jupyter_code>aut = spot.translate('FGa', 'generic', 'deterministic'); aut.show('.ba')<jupyter_output><empty_output><jupyter_text>Translation to co-Büchi automaton<jupyter_code>spot.translate('FGa', 'coBuchi').show('.ba')
spot.translate('FGa', 'coBuchi', 'deterministic').show('.ba')<jupyter_output><empty_output><jupyter_text>Adding an atomic proposition to all edges<jupyter_code>import buddy
b = buddy.bdd_ithvar(aut.register_ap('b'))
for e in aut.edges():
    e.cond &= b
aut<jupyter_output><empty_output><jupyter_text>Adding an atomic proposition to the edge between 0 and 1:<jupyter_code>c = buddy.bdd_ithvar(aut.register_ap('c'))
for e in aut.out(0):
    if e.dst == 1:
        e.cond &= c
aut<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.15124309392265192, 'fraction_numerical': 0.014042357274401474, 'mean_word_length': 6.6362038664323375, 'pattern_counts': {'":': 0, '<': 65, '<?xml version=': 0, '>': 68, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '16', 'dir': 'jupyter-structured-clean-dedup', 'id': '647868', 'license': 'MIT', 'n_tokens_mistral': 1596, 'n_tokens_neox': 1545, 'n_words': 417, 'path': 'spot/tests/python/automata.ipynb', 'repo_name': 'mcc-petrinets/formulas', 'size': '4344'}