ioltl.org 8.68 KB
Newer Older
1
#+TITLE: Common input and output options for LTL/PSL formulas
2
3
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
4

5
6
Spot supports different syntaxes for LTL/PSL formulas.  This page
documents the options, common to all tools where it makes sense, that
7
8
9
10
11
12
13
14
15
16
17
are used to specify input and output of formula.

* Common input options

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

#+BEGIN_SRC sh :results verbatim :exports results
ltl2tgba --help | sed -n '/Input options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
:   -f, --formula=STRING       process the formula STRING
18
19
20
21
:   -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; usea negative COL to drop the first
:                              line of the CSV file
22
23
24
25
:       --lbt-input            read all formulas using LBT's prefix syntax
:       --lenient              parenthesized blocks that cannot be parsed as
:                              subformulas are considered as atomic properties

26
=-f= is used to pass one formula on the command line, but this option can
27
28
29
30
31
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
32
33
34
35
36
37
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 [[file:csv.org][examples of reading or writing CSV
files on a separate page]].
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

** Default parser

Spot's default LTL parser is able to parse the syntaxes of many tools,
such as [[http://spinroot.com][Spin]], [[http://vlsi.colorado.edu/~rbloem/wring.html][Wring]], [[http://goal.im.ntu.edu.tw][Goal]], etc.  For instance here are the preferred ways
to express the same formula for different tools.

# <<tab:formula-syntaxes>>
| Tool         | Formula                 |
|--------------+-------------------------|
| 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
#+HTML: <code>"GFa"</code>
.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
69
These double-quote strings also make it possible to embed arbitrarily
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
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:

#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt -f '(a U b U) U c'
#+END_SRC
#+RESULTS:

#+BEGIN_SRC sh :results verbatim :exports results
(ltlfilt -f '(a U b U) U c' 2>&1 | cat) | sed '/^$/d'
#+END_SRC
#+RESULTS:
: >>> (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:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --lenient -f '(a U b U) U c'
#+END_SRC
#+RESULTS:
: "a U b U" U c

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

** Prefix parser

126
127
128
129
130
131
The prefix syntax used by tools such as [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]], [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], [[http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/][scheck]] or [[http://www.ltl2dstar.de][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.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132
133
134
135
136
137

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 operator (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
138
used by [[http://www.ltl2dstar.de][ltl2dstar]].
139
140
141

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

142

143
144
145
146
147
148
149
150
* Common output options

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

#+BEGIN_SRC sh :results verbatim :exports results
ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
151
152
153
154
155
156
157
158
159
160
161
162
#+begin_example
  -8, --utf8                 output using UTF-8 characters
      --csv                  quote the formula for use in a CSV file
      --format=FORMAT        specify how each line should be output (default:
                             "%f")
  -l, --lbt                  output in LBT's syntax
      --latex                output using LaTeX macros
  -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
#+end_example
163
164
165

#  LocalWords:  syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME

166
The =--spot=, =--utf-8=, =--spin=, =--wring= options select different
167
168
169
170
171
172
173
174
output syntaxes as seen in [[tab:formula-syntaxes][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.
175

176
Note that by default Spot always outputs parentheses around operators
177
178
179
180
181
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=.

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

185
186
187
188
189
190
191
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 [[file:csv.org][examples of reading or writing CSV files on a
separate page]].

192
193
194
195
196
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:

197
198
199
200
201
|           | =%f=           | =%F=           | =%L=              | =%<=         | =%>=          |
|-----------+----------------+----------------+-------------------+--------------+---------------|
| [[file:ltlfilt.org][=ltlfilt=]] | output formula | input filename | input line        | leading text | trailing text |
| [[file:genltl.org][=genltl=]]  | output formula | pattern name   | pattern parameter | (empty)      | (empty)       |
| [[file:randltl.org][=randltl=]] | output formula | (empty)        | formula number    | (empty)      | (empty)       |
202

203
204
#  LocalWords:  lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck
#  LocalWords:  utf associativity