Handling LTL and PSL formulas



In [1]:

    
import spot

For interactive use, formulas can be entered as text strings and passed to the spot.formula constructor.



In [2]:

    
f = spot.formula('p1 U p2 R (p3 & !p4)')
f









    Out[2]:





$p_{1} \mathbin{\mathsf{U}} (p_{2} \mathbin{\mathsf{R}} (p_{3} \land \lnot p_{4}))$



In [3]:

    
g = spot.formula('{a;b*;c[+]}<>->GFb'); g









    Out[3]:





$\{a \mathbin{\mathsf{;}} b^{\star} \mathbin{\mathsf{;}} c^+\}\mathrel{\Diamond\kern-1.7pt\raise.4pt\hbox{$\mathord{\rightarrow}$}} \mathsf{G} \mathsf{F} b$

By default the parser recognizes an infix syntax, but when this fails, it tries to read the formula with the LBT syntax:



In [4]:

    
h = spot.formula('& | a b c'); h









    Out[4]:





$c \land (a \lor b)$

By default, a formula object is presented using mathjax as above. When a formula is converted to string you get Spot's syntax by default:



In [5]:

    
str(f)









    Out[5]:





'p1 U (p2 R (p3 & !p4))'

If you prefer to print the string in another syntax, you may use the to_str() method, with an argument that indicates the output format to use. The latex format assumes that you will the define macros such as \U, \R to render all operators as you wish. On the otherhand, the sclatex (with sc for self-contained) format hard-codes the rendering of each of those operators: this is typically the output that is used to render formulas using MathJax in a notebook.



In [6]:

    
for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex']:
    print("%-10s%s" % (i, f.to_str(i)))









    



spot      p1 U (p2 R (p3 & !p4))
spin      p1 U (p2 V (p3 && !p4))
lbt       U p1 V p2 & p3 ! p4
wring     (p1=1) U ((p2=1) R ((p3=1) * (p4=0)))
utf8      p1 U (p2 R (p3∧¬p4))
latex     p_{1} \U (p_{2} \R (p_{3} \land \lnot p_{4}))
sclatex   p_{1} \mathbin{\mathsf{U}} (p_{2} \mathbin{\mathsf{R}} (p_{3} \land \lnot p_{4}))

Formulas output via format() can also use some convenient shorthand to select the syntax:



In [7]:

    
print("""\
Spin:               {0:s}
Spin+parentheses:   {0:sp}
Spot (default):     {0}
Spot+shell quotes:  {0:q}
LBT, right aligned: {0:l:~>40}
LBT, no M/W/R:      {0:[MWR]l}""".format(f))









    



Spin:               p1 U (p2 V (p3 && !p4))
Spin+parentheses:   (p1) U ((p2) V ((p3) && (!(p4))))
Spot (default):     p1 U (p2 R (p3 & !p4))
Spot+shell quotes:  'p1 U (p2 R (p3 & !p4))'
LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4
LBT, no M/W/R:      U p1 U & p3 ! p4 | & & p2 p3 ! p4 G & p3 ! p4

The specifiers that can be used with format are documented as follows:



In [8]:

    
help(spot.formula.__format__)









    



Help on function __format__ in module spot:

__format__(self, spec)
    Format the formula according to `spec`.
    
    Parameters
    ----------
    spec : str, optional
        a list of letters that specify how the formula
        should be formatted.
    
    Supported specifiers
    --------------------
    
    - 'f': use Spot's syntax (default)
    - '8': use Spot's syntax in UTF-8 mode
    - 's': use Spin's syntax
    - 'l': use LBT's syntax
    - 'w': use Wring's syntax
    - 'x': use LaTeX output
    - 'X': use self-contained LaTeX output
    
    Add some of those letters for additional options:
    
    - 'p': use full parentheses
    - 'c': escape the formula for CSV output (this will
           enclose the formula in double quotes, and escape
           any included double quotes)
    - 'h': escape the formula for HTML output
    - 'd': escape double quotes and backslash,
           for use in C-strings (the outermost double
           quotes are *not* added)
    - 'q': quote and escape for shell output, using single
           quotes or double quotes depending on the contents.
    - '[...]': rewrite away all the operators specified in brackets,
           using spot.unabbreviate().
    
    - ':spec': pass the remaining specification to the
               formating function for strings.

A spot.formula object has a number of built-in predicates whose value have been computed when the formula was constructed. For instance you can check whether a formula is in negative normal form using is_in_nenoform(), and you can make sure it is an LTL formula (i.e. not a PSL formula) using is_ltl_formula():



In [9]:

    
f.is_in_nenoform() and f.is_ltl_formula()









    Out[9]:





True



In [10]:

    
g.is_ltl_formula()









    Out[10]:





False

Similarly, is_syntactic_stutter_invariant() tells wether the structure of the formula guarranties it to be stutter invariant. For LTL formula, this means the X operator should not be used. For PSL formula, this function capture all formulas built using the siPSL grammar.



In [11]:

    
f.is_syntactic_stutter_invariant()









    Out[11]:





True



In [12]:

    
spot.formula('{a[*];b}<>->c').is_syntactic_stutter_invariant()









    Out[12]:





False



In [13]:

    
spot.formula('{a[+];b[*]}<>->d').is_syntactic_stutter_invariant()









    Out[13]:





True

spot.relabel renames the atomic propositions that occur in a formula, using either letters, or numbered propositions:



In [14]:

    
gf = spot.formula('(GF_foo_) && "a > b" && "proc[2]@init"'); gf









    Out[14]:





$``\mathit{a > b}\textrm{''} \land ``\mathit{proc[2]@init}\textrm{''} \land \mathsf{G} \mathsf{F} \mathit{\_foo\_}$



In [15]:

    
spot.relabel(gf, spot.Abc)









    Out[15]:





$a \land b \land \mathsf{G} \mathsf{F} c$



In [16]:

    
spot.relabel(gf, spot.Pnn)









    Out[16]:





$p_{0} \land p_{1} \land \mathsf{G} \mathsf{F} p_{2}$

The AST of any formula can be displayed with show_ast(). Despite the name, this is not a tree but a DAG, because identical subtrees are merged. Binary operators have their left and right operands denoted with L and R, while non-commutative n-ary operators have their operands numbered.



In [17]:

    
print(g); g.show_ast()









    



{a;b[*];c[+]}<>-> GFb






    Out[17]:

Any formula can also be classified in the temporal hierarchy of Manna & Pnueli



In [22]:

    
g.show_mp_hierarchy()









    Out[22]:



In [24]:

    
spot.mp_class(g, 'v')









    Out[24]:





'recurrence'



In [18]:

    
f = spot.formula('F(a & X(!a & b))'); f









    Out[18]:





$\mathsf{F} (a \land \mathsf{X} (\lnot a \land b))$

Etessami's rule for removing X (valid only in stutter-invariant formulas)



In [19]:

    
spot.remove_x(f)









    Out[19]:





$\mathsf{F} (a \land ((a \land (a \mathbin{\mathsf{U}} (\lnot a \land b)) \land ((\lnot b \mathbin{\mathsf{U}} \lnot a) \lor (b \mathbin{\mathsf{U}} \lnot a))) \lor (\lnot a \land (\lnot a \mathbin{\mathsf{U}} (a \land \lnot a \land b)) \land ((\lnot b \mathbin{\mathsf{U}} a) \lor (b \mathbin{\mathsf{U}} a))) \lor (b \land (b \mathbin{\mathsf{U}} (\lnot a \land b \land \lnot b)) \land ((\lnot a \mathbin{\mathsf{U}} \lnot b) \lor (a \mathbin{\mathsf{U}} \lnot b))) \lor (\lnot b \land (\lnot b \mathbin{\mathsf{U}} (\lnot a \land b)) \land ((\lnot a \mathbin{\mathsf{U}} b) \lor (a \mathbin{\mathsf{U}} b))) \lor (\lnot a \land b \land (\mathsf{G} \lnot a \lor \mathsf{G} a) \land (\mathsf{G} \lnot b \lor \mathsf{G} b))))$

Removing abbreviated operators



In [20]:

    
f = spot.formula("G(a xor b) -> F(a <-> b)")
spot.unabbreviate(f, "GF^")









    Out[20]:





$(\bot \mathbin{\mathsf{R}} \lnot (a \leftrightarrow b)) \rightarrow (\top \mathbin{\mathsf{U}} (a \leftrightarrow b))$



In [21]:

    
spot.unabbreviate(f, "GF^ei")









    Out[21]:





$(\top \mathbin{\mathsf{U}} ((a \land b) \lor (\lnot a \land \lnot b))) \lor \lnot (\bot \mathbin{\mathsf{R}} ((\lnot a \land b) \lor (a \land \lnot b)))$