To build an automaton from an LTL formula, 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).

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.

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:

The translate() function can also be called with a formula object. Either as a function, or as a method.

When used as a method, all the arguments are translation options. Here is a monitor:

The following three cells show a formulas for which it makes a difference to select 'small' or 'deterministic'.

Here is how to build an unambiguous automaton:

Compare with the standard translation:

And here is the automaton above with state-based acceptance:

Some example of running the self-loopization algorithm on an automaton:

Reading from file (see automaton-io.ipynb for more examples).

Explicit determinization after translation:

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

Translation to state-based co-Büchi automaton

Translation to parity automaton. Specifying just parity max odd requires a parity acceptance. Adding colored ensures that each transition (or state if sbacc is also given) has a color, as people usually expect in parity automata.

Adding an atomic proposition to all edges

Adding an atomic proposition to the edge between 0 and 1: