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]:
Inf( ⓿ ) [Büchi] 0 0 I->0 1 1 0->1 !a 2 2 1->2 !a 3 3 1->3 a 4 4 1->4 !a 2->2 !a & b 2->3 a & b ⓿ 3->2 !a & b 3->3 a & b ⓿ 5 5 3->5 !a & b 4->4 !a & !b ⓿ 5->4 !a & b

Build an accepting run:

In [3]:
run = aut.accepting_run()
print(run)

Prefix:
  0
  |  !a
  1
  |  !a
Cycle:
  2
  |  a & b	{0}
  3
  |  !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 literals. The word is just the projection of the run on its labels.

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

!a; !a; cycle{a & b; !a & b}
Out[5]:
$\lnot a; \lnot a; \mathsf{cycle}\{a \land b; \lnot 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 [6]:
word.show()
Out[6]:
abprefixcycle cycle

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]))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))

!a
!a
a & b
!a & b

Calling simplify() will produce a shorter word that is compatible with the original word. For instance, in the above word the second a is compatible with !a & b, so the prefix can be shortened by rotating the cycle.

In [8]:
word.simplify()
print(word)

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

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

In [9]:
aut.accepting_word()
Out[9]:
$\lnot a; \mathsf{cycle}\{\lnot a \land b; a \land 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 \land b; \mathsf{cycle}\{\lnot a \land \lnot b; \lnot a \land b\}$
In [12]:
w.show()
Out[12]:
abprefixcycle cycle

Words can be easily converted to automata

In [13]:
w.as_automaton()
Out[13]:
t [all] 0 0 I->0 1 1 0->1 a 2 2 1->2 a & b 3 3 2->3 !a & !b 3->2 !a & b

To check if a word is accepted by an automaton, you can use intersects. The name intersects actually makes more sense than accepts or accepted, because a word actually describes a set of words because of the don't care atomic propositions.

In [16]:
print(w.intersects(aut))
print(aut.intersects(w))
print(word.intersects(aut))
print(aut.intersects(word))

False
False
True
True
In [ ]: