For a more precise description of Spot's temporal operators, including PSL operators, GetSpot and read the included file doc/tl/tl.pdf.

The LTL parser used in Spot understands a mix of the syntaxes used by several other tools (notably Spin, Wring, ltl2ba), so you can use whichever you prefer. This is the reason why some operators have several variants. For instance Spot will understand []<>a as well as GFa. Similarly, p0 U !p1 is just the same as p0=1Up1=0. However allowing formulae like GFa introduces some quirks in the way atomic propositions can be named.

1. Unary prefix operators

2. Unary postfix operators

These two operators are needed to parse Wring's LTL formulae.

3. Binary operators

4. Constants

These are case-insensitive, while the other operators are not.

5. Naming atomic propositions

Any alphanumeric identifier that does not start with a digit or with the letter of a unary prefix operator (F, G, or X) can be used as an atomic proposition. Other propositions must be double-quoted. For instance if GFa is the name of an atomic proposition that must be true infinitely often, the LTL formula is GF"GFa".

As a special exception to the above rule, atomic propositions can start with F, G, or X without requiring quotes if the second character is a digit. This allow naming atomic propositions X0, X1, X2, etc. This also means that X(0) is not the same as X0 (but who would use X(0)?)

Note that infix operator letters do not break identifiers. So aUb is an atomic proposition, unlike the formulae a U b, (a)U(b), and even a=1Ub=1.

LtlSyntax (last edited 2012-06-02 10:07:51 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.