ioltl.org 11.2 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: Common input and output options for LTL/PSL formulas
3
#+DESCRIPTION: Options for input and output of temporal logic formulas in Spot's command-line tools
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
5
#+HTML_LINK_UP: tools.html
6

7
8
Spot supports different syntaxes for LTL/PSL formulas.  This page
documents the options, common to all tools where it makes sense, that
9
10
11
12
13
14
15
16
17
18
19
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
20
21
22
23
:   -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
24
25
26
27
:       --lbt-input            read all formulas using LBT's prefix syntax
:       --lenient              parenthesized blocks that cannot be parsed as
:                              subformulas are considered as atomic properties

28
=-f= is used to pass one formula on the command line, but this option can
29
30
31
32
33
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
34
35
36
37
38
39
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]].
40
41
42
43
44
45
46

** 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
47
#+NAME: tab:formula-syntaxes
48
49
50
51
52
53
54
55
56
57
58
| 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
60
operators, please refer to the
[[https://spot.lrde.epita.fr/tl.pdf][=doc/tl/tl.pdf= document inside the Spot distribution]].
61
62
63
64
65
66
67
68
69
70

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
71
These double-quote strings also make it possible to embed arbitrarily
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
126
127
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

128
129
130
131
132
133
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
134
135
136
137
138
139

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
140
used by [[http://www.ltl2dstar.de][ltl2dstar]].
141
142
143

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

144

145
146
147
148
149
* Common output options

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

#+BEGIN_SRC sh :results verbatim :exports results
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
150
genltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
151
152
#+END_SRC
#+RESULTS:
153
#+begin_example
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154
155
  -0, --zero-terminated-output   separate output formulas with \0 instead of \n
                             (for use with xargs -0)
156
  -8, --utf8                 output using UTF-8 characters
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
      --csv-escape           quote the formula for use in a CSV file
158
159
160
161
      --format=FORMAT        specify how each line should be output (default:
                             "%f")
  -l, --lbt                  output in LBT's syntax
      --latex                output using LaTeX macros
162
163
164
  -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 '>>'.
165
166
167
168
169
  -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
170

171
The =--spot=, =--utf-8=, =--spin=, =--wring= options select different
172
173
174
175
176
177
178
179
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.
180

181
Note that by default Spot always outputs parentheses around operators
182
183
184
185
186
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=.

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

190
191
192
193
194
195
196
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]].

197
198
199
200
201
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:

202
203
204
205
206
207
|            | =%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)       |
| [[file:ltlfilt.org][=ltlgrind=]] | output formula | input filename | input line        | leading text | trailing text |
208

209
Other =%=-sequences are supported by these tools, and documented in
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
210
211
the output of =--help=.  For instance =%s= can be used to compute the
size of a formula.
212
213

By default everything is output to standard output, so that you can
214
redirect the output to a file, and pipe it to another tool.  The
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
=--output= (or =-o=) allows you to construct a filename using some of
the above =%=-sequences.

For instance the following invocation of [[file:randltl.org][=randltl=]] will create 5
random formulas, but in 5 different files:

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n5 a b -o example-%L.ltl
wc -l example-*.ltl
#+END_SRC
#+RESULTS:
:  1 example-1.ltl
:  1 example-2.ltl
:  1 example-3.ltl
:  1 example-4.ltl
:  1 example-5.ltl
:  5 total

233
#+BEGIN_SRC sh :results silent :exports results
234
235
236
237
rm -f example-*.ltl
#+END_SRC
#+RESULTS:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
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:

#+BEGIN_SRC sh :results verbatim :exports both
genltl -0 --gh-q=1..4 | xargs -0 ltl2tgba --stats='%F,%f,%s'
genltl --gh-q=1..4 | ltl2tgba -F- --stats='%F,%f,%s'
#+END_SRC

#+RESULTS:
: ,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 =-=).


265

266
267
#  LocalWords:  lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck
#  LocalWords:  utf associativity
268
#  LocalWords:  syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME