In [1]:
import spot
from spot.jupyter import display_inline
spot.setup(show_default='.a')

Containement checks

The spot.contains() function checks whether the language of its right argument is included in the language of its left argument. The arguments may mix automata and formulas; the latter can be given as strings.

In [2]:
f = spot.formula('GFa'); aut_f = f.translate()
g = spot.formula('FGa'); aut_g = g.translate()
In [3]:
spot.contains(f, g), spot.contains(g, f)
Out[3]:
(True, False)
In [4]:
spot.contains(aut_f, aut_g), spot.contains(aut_g, aut_f)
Out[4]:
(True, False)
In [5]:
spot.contains(aut_f, g), spot.contains(aut_g, f)
Out[5]:
(True, False)
In [6]:
spot.contains(f, aut_g), spot.contains(g, aut_f)
Out[6]:
(True, False)
In [7]:
spot.contains("GFa", aut_g), spot.contains("FGa", aut_f)
Out[7]:
(True, False)

Those functions are also usable as methods:

In [8]:
f.contains(aut_g), g.contains(aut_f)
Out[8]:
(True, False)
In [9]:
aut_f.contains("FGa"), aut_g.contains("GFa")
Out[9]:
(True, False)

Equivalence checks

The spot.are_equivalent() tests the equivalence of the languages of its two arguments. Note that the corresponding method is called equivalent_to().

In [10]:
spot.are_equivalent(f, g), spot.are_equivalent(aut_f, aut_g)
Out[10]:
(False, False)
In [11]:
f.equivalent_to(aut_g), aut_f.equivalent_to(g)
Out[11]:
(False, False)
In [12]:
aut_f.equivalent_to('XXXGFa')
Out[12]:
True

Containement checks between formulas with cache

In the case of containement checks between formulas, language_containement_checker instances provide similar services, but they cache automata representing the formulas checked. This should be preferred when performing several containement checks using the same formulas.

In [13]:
lcc = spot.language_containment_checker()
In [14]:
lcc.contains(f, g), lcc.contains(g, f)
Out[14]:
(True, False)
In [15]:
lcc.are_equivalent(f, g)
Out[15]:
False

Help for distinguishing languages

Assume you have computed two automata, that are_equivalent(a1, a2) returns False, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called a1.exclusive_run(a2) that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method a1.exclusive_word(a2) will return just a word.

For instance let's find a word that is exclusive between aut_f and aut_g. (The adjective exclusive is a reference to the exclusive or operator: the word belongs to L(aut_f) "xor" it belongs to L(aut_g).)

In [16]:
aut_f.exclusive_word(aut_g)
Out[16]:
$\mathsf{cycle}\{a; \lnot a\}$

We can even write a small function that highlights one difference between two automata. Note that the run returned will belong to either left or right, so calling the highlight() method will colorize one of those two automata.

In [17]:
def show_one_difference(left, right):
    run = left.exclusive_run(right)
    if not run:
        print("The two automata are equivalent.")
    else:
        print("The following word is only accepted by one automaton:", spot.make_twa_word(run))
        run.highlight(5)
        display_inline(left, right)
In [18]:
show_one_difference(aut_f, aut_g)

The following word is only accepted by one automaton: cycle{a; !a}
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 !a 0->0 a ⓿
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 a 1->1 a