Common input and output options for LTL/PSL formulas

Table of Contents

Spot supports different syntaxes for LTL/PSL formulas. This page documents the options, common to all tools where it makes sense, that are used to specify input and output of formula.

Common input options

All tools that read LTL/PSL formulas implement the following options:

-f, --formula=STRING       process the formula STRING
-F, --file=FILENAME[/COL]  process each line of FILENAME as a formula; if COL
                           is a positive integer, assume a CSV file and read
                           column COL; use a negative COL to drop the first
                           line of the CSV file
    --lbt-input            read all formulas using LBT's prefix syntax
    --lenient              parenthesized blocks that cannot be parsed as
                           subformulas are considered as atomic properties
    --negate               negate each formula

-f is used to pass one formula on the command line, but this option can be repeated to pass multiple formulas.

-F is used to read formulas from a file (one formula per line). This option can also be repeated to pass multiple files. If the filename specified is - (as in -F-), then formulas are read from standard input. If a filename is suffixed with /COL, where COL is a positive integer, then the file is assumed to be a CSV file, and formulas are read from its COL-th column. Use /-COL to read from column COL and ignore the first line of the CSV file (which often contains column headers). We have examples of reading or writing CSV files on a separate page.

Default parser

Spot's default LTL parser is able to parse the syntaxes of many tools, such as Spin, Wring, Goal, etc. For instance here are the preferred ways to express the same formula for different tools.

Spot G(a -> (b R !c))
Spot (UTF-8) □(a → (b R c̅))
Spin [](a -> (b V !c))
Wring G(a=1 -> (b=1 R c=0))
Goal G(a --> (b R ~c))

Spot's default LTL parser will understand all of them.

For a complete definition of the supported operators, including PSL operators, please refer to the doc/tl/tl.pdf document inside the Spot distribution.

For Spot, an atomic proposition is any alphanumeric string that does not start with the (upper case) characters F, G, or X. For instance gfa is an atomic proposition, but GFa actually denotes the LTL formula G(F(a)). Any double-quoted string is also considered to be an atomic proposition, so if GFa had to be an atomic proposition, it could be written "GFa":.

These double-quote strings also make it possible to embed arbitrarily complex expressions that represent an atomic proposition that Spot should not try to interpret. For instance:

"a < b" U "process[2]@ok"

Lenient mode

In version 6, Spin extended its syntax to support arbitrary atomic expression in LTL formulas. The previous formula would be written simply:

(a < b) U (process[2]@ok)

While Spot cannot read the above syntax by default, it can do it if you specify the --lenient option. (This global option affects all formulas that are input.)

The same parser is used, however its processing of parenthesis blocks is different: every time a parenthesis block is scanned, the parser first tries to recursively parse the block as an LTL/PSL formula, and if this parsing failed, the block is considered to be an atomic proposition.

For instance (a U b) U c will be successfully converted into an LTL formula with two operators, while parsing (a + b < 2) U c will consider a + b < 2 as an atomic proposition.

An unfortunate side-effect of --lenient parsing is that many syntax errors will not be caught. Compare the following syntax error:

ltlfilt -f '(a U b U) U c'
>>> (a U b U) U c
syntax error, unexpected closing parenthesis

>>> (a U b U) U c
missing right operand for "until operator"

With the same command in --lenient mode:

ltlfilt --lenient -f '(a U b U) U c'
"a U b U" U c

Here a U b U was taken as an atomic proposition.

Prefix parser

The prefix syntax used by tools such as LBT, LBTT, scheck or ltl2dstar requires a different parser. For these tools, the above example formula has to be written G i p0 V p1 ! p2 (in LBT's syntax, atomic propositions must start with p and be followed by a number). Spot's --lbt-input option can be used to activate the parser for this syntax.

The following operators are supported:

t true
f false
! not
& and
| or
^ xor
i implies
e equivalent
X next
F eventually
G globally
U strong until
V weak release
M strong release
W weak until

As an extension to LBT's syntax, alphanumeric atomic propositions that follow the "p + number" rule will be accepted if they do not conflict with one of the operators (e.g., i, the implies operator, cannot be used as an atomic proposition). Also any atomic proposition may be double-quoted. These extensions are compatible with the syntax used by ltl2dstar.

--lbt-input is a global option that affects all formulas that are read.

Common output options

All tools that output LTL/PSL formulas implement the following options:

-0, --zero-terminated-output   separate output formulas with \0 instead of \n
                           (for use with xargs -0)
-8, --utf8                 output using UTF-8 characters
    --format=FORMAT, --stats=FORMAT
                           specify how each line should be output (default:
-l, --lbt                  output in LBT's syntax
    --latex                output using LaTeX macros
-o, --output=FORMAT        send output to a file named FORMAT instead of
                           standard output.  The first formula sent to a file
                           truncates it unless FORMAT starts with '>>'.
-p, --full-parentheses     output fully-parenthesized formulas
-s, --spin                 output in Spin's syntax
    --spot                 output in Spot's syntax (default)
    --wring                output in Wring's syntax

The --spot, --utf-8, --spin, --wring options select different output syntaxes as seen in the above table.

Option --latex causes formulas to be output using LaTeX macros for each operator. You may define these macros as you wish, and some example definitions are in doc/tl/spotltl.sty.

The -p option can be used to request that parentheses be used at all levels.

Note that by default Spot always outputs parentheses around operators such as U, because not all tools agree on their associativity. For instance a U b U c is read by Spot as a U (b U c) (because U is right-associative in the PSL standard), while Spin (among other tools) with read it as (a U b) U c.

The --lbt option requests an output in LBT's prefix format, and in that case discussing associativity and parentheses makes no sense.

The --csv causes the formulas to be double-quoted (with inner double-quotes doubled, as per RFC 4180), regardless of the selected format. This is needed if the formula should appear in a CSV file, and you want to be robust to formulas that contains commas or double-quotes. We have examples of reading or writing CSV files on a separate page.

The --format option can be used to fine-tune the way the formula is output. Not using the --format option is equivalent to using --format=%f. The semantic of the available %-sequences differ from tool to tool:

ltlfilt output formula input filename input line leading text trailing text
genltl output formula pattern name pattern parameter (empty) (empty)
randltl output formula (empty) formula number (empty) (empty)
ltlgrind output formula input filename input line leading text trailing text

Other %-sequences are supported by these tools, and documented in the output of --help. For instance %s can be used to compute the size of a formula.

By default everything is output to standard output, so that you can redirect the output to a file, and pipe it to another tool. The --output (or -o) allows you to construct a filename using some of the above %-sequences.

For instance the following invocation of randltl will create 5 random formulas, but in 5 different files:

randltl -n5 a b -o example-%L.ltl
wc -l example-*.ltl
1 example-1.ltl
1 example-2.ltl
1 example-3.ltl
1 example-4.ltl
1 example-5.ltl
5 total

Option -0 is useful if the list of formulas is passed to xargs. xargs normally splits its input on white space (which are frequent in LTL formulas), but you can use xargs -0 to split the input on null characters. So for instance the following two invocations have nearly the same output:

genltl -0 --gh-q=1..4 | xargs -0 ltl2tgba --stats='%F,%f,%s'
genltl --gh-q=1..4 | ltl2tgba -F- --stats='%F,%f,%s'
,Fp1 | Gp2,3
,(Fp1 | Gp2) & (Fp2 | Gp3),8
,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4),18
,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4) & (Fp4 | Gp5),42
-,Fp1 | Gp2,3
-,(Fp1 | Gp2) & (Fp2 | Gp3),8
-,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4),18
-,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4) & (Fp4 | Gp5),42

The only difference is that for the first command, ltl2tgba received its formulas from the command-line arguments supplied by xargs (so %F is empty as there is no input file), while in the second case the formula where read from standard input (denoted by -).