Handling LTL and PSL formulas

In [1]:
import spot
from IPython.display import display # not needed with recent Jupyter

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;first_match((b*;c[+])[:*3..5];b)}<>->(GFb & c)'); g
Out[3]:
$\{a \mathbin{\mathsf{;}} \mathsf{first\_match}(\{b^{\star} \mathbin{\mathsf{;}} c^+\}^{\mathsf{:}\star3..5} \mathbin{\mathsf{;}} b)\}\mathrel{\Diamond\kern-1.7pt\raise.4pt\hbox{$\mathord{\rightarrow}$}} (c \land \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)$

Passing a formula to spot.formula simply returns the formula.

In [5]:
spot.formula(h)
Out[5]:
$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 [6]:
str(f)
Out[6]:
'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 almost the same output that is used to render formulas using MathJax in a notebook. sclatex and mathjax only differ in the rendering of double-quoted atomic propositions.

In [7]:
for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:
    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}))
mathjax   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 [8]:
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 [9]:
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
    - 'j': use self-contained LaTeX output, adjusted for MathJax
    
    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 [10]:
f.is_in_nenoform() and f.is_ltl_formula()
Out[10]:
True
In [11]:
g.is_ltl_formula()
Out[11]:
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 [12]:
f.is_syntactic_stutter_invariant()
Out[12]:
True
In [13]:
spot.formula('{a[*];b}<>->c').is_syntactic_stutter_invariant()
Out[13]:
False
In [14]:
spot.formula('{a[+];b[*]}<>->d').is_syntactic_stutter_invariant()
Out[14]:
True

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

In [15]:
gf = spot.formula('(GF_foo_) && "a > b" && "proc[2]@init"'); gf
Out[15]:
$\unicode{x201C}\mathit{a > b}\unicode{x201D} \land \unicode{x201C}\mathit{proc[2]@init}\unicode{x201D} \land \mathsf{G} \mathsf{F} \mathit{\_foo\_}$
In [16]:
spot.relabel(gf, spot.Abc)
Out[16]:
$a \land b \land \mathsf{G} \mathsf{F} c$
In [17]:
spot.relabel(gf, spot.Pnn)
Out[17]:
$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 [18]:
print(g); g.show_ast()

{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)
Out[18]:
G 0 EConcat 1 Concat 0->1 L 11 And 0->11 R 2 a 1->2 1 3 first_match 1->3 2 4 Concat 3->4 5 FStar 3..5 4->5 1 8 b 4->8 2 6 Concat 5->6 7 Star 6->7 1 9 Star 1.. 6->9 2 7->8 10 c 9->10 11->10 12 G 11->12 13 F 12->13 13->8

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

In [19]:
g.show_mp_hierarchy()
Out[19]:
Reactivity Recurrence Persistence Obligation Safety Guarantee Monitor Deterministic Büchi Terminal Büchi Weak Büchi
In [20]:
spot.mp_class(g, 'v')
Out[20]:
'recurrence'
In [21]:
f = spot.formula('F(a & X(!a & b))'); f
Out[21]:
$\mathsf{F} (a \land \mathsf{X} (\lnot a \land b))$

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

In [22]:
spot.remove_x(f)
Out[22]:
$\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 [23]:
f = spot.formula("G(a xor b) -> F(a <-> b)")
spot.unabbreviate(f, "GF^")
Out[23]:
$(\bot \mathbin{\mathsf{R}} \lnot (a \leftrightarrow b)) \rightarrow (\top \mathbin{\mathsf{U}} (a \leftrightarrow b))$
In [24]:
spot.unabbreviate(f, "GF^ei")
Out[24]:
$(\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)))$

Nesting level of operators

In [25]:
f = spot.formula('F(b & X(a U b U ((a W Fb) | (c U d))))')
print("U", spot.nesting_depth(f, spot.op_U))
print("F", spot.nesting_depth(f, spot.op_F))
# These following two are syntactic sugar for the above two
print("U", spot.nesting_depth(f, "U"))
print("F", spot.nesting_depth(f, "F"))
# If you want to consider "U" and "F" are a similar type of
# operator, you can count both with
print("FU", spot.nesting_depth(f, "FU"))

U 3
F 2
U 3
F 2
FU 4

Collecting the set of atomic propositions used by a formula:

In [26]:
ap = spot.atomic_prop_collect(f)
print(repr(ap))  # print as an atomic_prop_set object
print(ap)        # print as a string
display(ap)      # LaTeX-style, for notebooks

spot.atomic_prop_set([spot.formula("a"), spot.formula("b"), spot.formula("c"), spot.formula("d")])
{"a", "b", "c", "d"}
$\{\unicode{x201C}a\unicode{x201D}, \unicode{x201C}b\unicode{x201D}, \unicode{x201C}c\unicode{x201D}, \unicode{x201C}d\unicode{x201D}\}$

Converting to Suffix Operator Normal Form:

In [27]:
f = spot.formula('G({x*} []-> Fa)')
display(f)

# In addition to the formula, returns a list of newly introduced APs
f, aps = spot.suffix_operator_normal_form(f, 'sonf_')
display(f)
display(aps)
$\mathsf{G} (\{x^{\star}\}\mathrel{\Box\kern-1.7pt\raise.4pt\hbox{$\mathord{\rightarrow}$}} \mathsf{F} a)$
$\mathsf{G} \mathit{sonf\_}_{0} \land \mathsf{G} (\lnot \mathit{sonf\_}_{1} \lor \mathsf{F} a) \land \mathsf{G} (\lnot \mathit{sonf\_}_{0} \lor (\{x^{\star}\}\mathrel{\Box\kern-1.7pt\raise.4pt\hbox{$\mathord{\rightarrow}$}} \mathit{sonf\_}_{1}))$ 
('sonf_0', 'sonf_1')