In [1]: 
import spot
spot.setup()

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

In [2]: 
aut = spot.translate('G(Fa <-> Xb)'); aut
Out[2]:
G 0 0 I->0 1 1 0->1 !a 2 2 0->2 a 3 3 0->3 !a 1->1 !a & b 1->2 a & b ⓿ 2->1 !a & b 2->2 a & b ⓿ 2->3 !a & b 3->3 !a & !b ⓿

Build an accepting run:

In [3]: 
run = aut.accepting_run(); run
Out[3]:
Prefix:
  0
  |  !a
Cycle:
  1
  |  a & b	{0}
  2
  |  !a & b

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

In [4]: 
print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))
print(run.cycle[0].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 [5]: 
word = spot.twa_word(run); word
Out[5]:
!a; cycle{a & b; !a & b}

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

In [6]: 
print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))

!a
a & b
!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, but it allows removing the prefix by rotating the cycle:

In [7]: 
word.simplify()
word
Out[7]:
cycle{!a & b; a & b}

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

In [8]: 
aut.accepting_word()
Out[8]:
cycle{!a & b; a & b}

Words can be created using the parse_word function:

In [9]: 
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 [10]: 
# make sure that we can parse a word back after it has been printed
spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b}')))
Out[10]:
a; a & b; cycle{!a & !b}

Words can be easily converted as automata

In [11]: 
w1 = spot.parse_word('a; !a; cycle{a; !a; a}')
In [12]: 
w1.as_automaton()
Out[12]:
G 0 0 I->0 1 1 0->1 a 2 2 1->2 !a 3 3 2->3 a 4 4 3->4 !a 4->2 a

The rest of this pages tests some syntax errors, you (humans) may skip it, but the test suite will not.

In [13]: 
print(spot.parse_word('a; b&!a; b'))

  File "<string>", line unknown
SyntaxError: 
>>> a; b&!a; b
              ^
A twa_word must contain a cycle
In [14]: 
print(spot.parse_word('a; b; c}'))

  File "<string>", line unknown
SyntaxError: 
>>> a; b; c}
           ^
Expected ';' delimiter: '}' stands for ending a cycle
In [15]: 
print(spot.parse_word('a; cycle{}'))

  File "<string>", line unknown
SyntaxError: 
>>> a; cycle{}
             ^
empty input
In [16]: 
print(spot.parse_word('a; cycle{!a}; a'))

  File "<string>", line unknown
SyntaxError: 
>>> a; cycle{!a}; a
                ^
Input should be finished after cycle
In [17]: 
# Creating an empty word is OK...
w = spot.twa_word(spot._bdd_dict)
In [18]: 
# ... as long as this word is not printed.
print(w)

---------------------------------------------------------------------------
RuntimeError                              Traceback (most recent call last)
<ipython-input-18-971829bb8f5f> in <module>()
      1 # ... as long as this word is not printed.
----> 2 print(w)

/home/adl/git/spot/python/spot/impl.py in __str__(self)
   3599 
   3600     def __str__(self) -> "std::string":
-> 3601         return _impl.twa_word___str__(self)
   3602 twa_word_swigregister = _impl.twa_word_swigregister
   3603 twa_word_swigregister(twa_word)

RuntimeError: a twa_word may not have an empty cycle