notebook.community

Edit and run

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".



In [1]:

    
import spot
spot.setup(show_default='.abr')



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



In [4]:

    
def implies(f, g):
    f = spot.formula(f)
    g = spot.formula_Not(spot.formula(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