

In [1]:

    
import spot
spot.setup()

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



In [2]:

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









    Out[2]:

Build an accepting run:



In [3]:

    
run = aut.accepting_run(); run









    Out[3]:





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 [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; a; cycle{a & b}

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



In [6]:

    
word.show()









    Out[6]:

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



In [7]:

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









    



!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 [8]:

    
word.simplify()
word









    Out[8]:





!a; cycle{a & b}

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



In [9]:

    
aut.accepting_word()









    Out[9]:





!a; cycle{a & b}

Words can be created using the parse_word function:



In [10]:

    
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 [11]:

    
# 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[11]:





a; a & b; cycle{!a & !b; !a & b}



In [12]:

    
w.show()









    Out[12]:

Words can be easily converted as automata



In [13]:

    
w.as_automaton()









    Out[13]: