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 lbtinput 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.
Tool 
Formula 

Spot  G(a > (b R !c)) 
Spot (UTF8)  □(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 doublequoted string is also
considered to be an atomic proposition, so if GFa
had to be an
atomic proposition, it could be written
"GFa":
.
These doublequote 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 sideeffect 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
lbtinput
option can be used to activate the parser for this
syntax.
The following operators are supported:
syntax 
meaning 

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 doublequoted. These extensions are compatible with the syntax
used by ltl2dstar.
lbtinput
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, zeroterminatedoutput separate output formulas with \0 instead of \n (for use with xargs 0) 8, utf8 output using UTF8 characters format=FORMAT, stats=FORMAT specify how each line should be output (default: "%f") 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, fullparentheses output fullyparenthesized formulas s, spin output in Spin's syntax spot output in Spot's syntax (default) wring output in Wring's syntax
The spot
, utf8
, 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
rightassociative 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 doublequoted (with inner
doublequotes 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
doublequotes. We have examples of reading or writing CSV files on a
separate page.
The format
option can be used to finetune 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:
%f 
%F 
%L 
%< 
%> 


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 example1.ltl 1 example2.ltl 1 example3.ltl 1 example4.ltl 1 example5.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 ghq=1..4  xargs 0 ltl2tgba stats='%F,%f,%s' genltl ghq=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 commandline 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 
).