In :
import spot
spot.setup()


Let's build a small automaton to use as example.

In :
aut = spot.translate('!a & G(Fa <-> XXb)'); aut

Out:

Build an accepting run:

In :
run = aut.accepting_run()
print(run)

Prefix:
0
|  !a
1
|  a
Cycle:
2
|  a & b	{0}



Accessing the contents of the run can be done via the prefix and cycle lists.

In :
print(spot.bdd_format_formula(aut.get_dict(), run.prefix.label))
print(run.cycle.acc)

!a
{0}


To convert the run into a word, using spot.twa_word(). Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels.

In :
word = spot.twa_word(run)
print(word)           # print as a string
word                  # LaTeX-style representation in notebooks

!a; a; cycle{a & b}

Out:
$\lnot a; a; \mathsf{cycle}\{a \land b\}$

A word can be represented as a collection of signals (one for each atomic proposition). The cycle part is shown twice.

In :
word.show()

Out:

Accessing the different formulas (stored as BDDs) can be done again via the prefix and cycle lists.

In :
print(spot.bdd_format_formula(aut.get_dict(), word.prefix))
print(spot.bdd_format_formula(aut.get_dict(), word.prefix))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle))

!a
a
a & b


Calling simplifify() will produce a shorter word that is compatible with the original word. For instance in the above word, the initial a is compatible with both a & b and a & !b. The word obtained by restricting a to a & b is therefore still accepted, allowing us to remove the prefix.

In :
word.simplify()
print(word)

!a; cycle{a & b}


Such a simplified word can be created directly from the automaton:

In :
aut.accepting_word()

Out:
$\lnot a; \mathsf{cycle}\{a \land b\}$

Words can be created using the parse_word function:

In :
print(spot.parse_word('a; b; cycle{a&b}'))
print(spot.parse_word('cycle{a&bb|bac&(aaa|bbb)}'))
print(spot.parse_word('a; b;b; qiwuei;"a;b&c;a" ;cycle{a}'))

a; b; cycle{a & b}
cycle{(a & bb) | (aaa & bac) | (bac & bbb)}
a; b; b; qiwuei; "a;b&c;a"; cycle{a}

In :
# make sure that we can parse a word back after it has been printed
w = spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b;!a&b}'))); w

Out:
$a; a \land b; \mathsf{cycle}\{\lnot a \land \lnot b; \lnot a \land b\}$
In :
w.show()

Out:

Words can be easily converted to automata

In :
w.as_automaton()

Out: