This example is the left part of Fig.2 in our ATVA'16 paper titled "Spot 2.0 — a framework for LTL and ω-automata manipulation", slightly updated to the current version of Spot.

In [1]:
import spot
spot.setup(show_default='.b')
In [2]:
f = spot.formula('GFa <-> GFb'); f
Out[2]:
$\mathsf{G} \mathsf{F} a \leftrightarrow \mathsf{G} \mathsf{F} b$
In [3]:
f.translate()
Out[3]:
Inf( ⓿ )&Inf( ❶ ) [gen. Büchi 2] 0 0 I->0 0->0 1 1 1 0->1 a | b 2 2 0->2 !a & !b 1->1 !a & !b 1->1 a & !b ⓿ 1->1 !a & b ❶ 1->1 a & b ⓿ ❶ 2->2 !a & !b ⓿ ❶
In [4]:
def implies(f, g):
    f = spot.formula(f)
    g = spot.formula.Not(g)
    return spot.product(f.translate(), g.translate()).is_empty()
def equiv(f, g):
    return implies(f, g) and implies(g, f)
In [5]:
equiv('a U (b U a)', 'b U a')
Out[5]:
True
In [6]:
equiv('!(a U b)', '!a U !b')
Out[6]:
False