Handling LTL and PSL formulas

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

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

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

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:

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.

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

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

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():

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.

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

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.

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

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

Removing abbreviated operators

Nesting level of operators

Collecting the set of atomic propositions used by a formula: