ioltl.org 11.7 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
#+PROPERTY: header-args:sh :results verbatim :exports both
7

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

* Common input options

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

16
#+BEGIN_SRC sh :exports results
17
18
19
20
ltl2tgba --help | sed -n '/Input options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
:   -f, --formula=STRING       process the formula STRING
21
22
:   -F, --file=FILENAME[/COL]  process each line of FILENAME as a formula; if COL
:                              is a positive integer, assume a CSV file and read
23
:                              column COL; use a negative COL to drop the first
24
:                              line of the CSV file
25
26
27
28
:       --lbt-input            read all formulas using LBT's prefix syntax
:       --lenient              parenthesized blocks that cannot be parsed as
:                              subformulas are considered as atomic properties

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

** Default parser
43
44
45
46
47
   :PROPERTIES:
   :CUSTOM_ID: infix
   :END:


48
49
50
51
52

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
53
#+NAME: tab:formula-syntaxes
54
55
56
57
58
59
60
61
62
63
64
| 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
65
66
operators, please refer to the
[[https://spot.lrde.epita.fr/tl.pdf][=doc/tl/tl.pdf= document inside the Spot distribution]].
67
68
69
70
71
72
73
74
75
76

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
77
These double-quote strings also make it possible to embed arbitrarily
78
79
80
81
82
complex expressions that represent an atomic proposition that Spot
should not try to interpret.  For instance:
: "a < b" U "process[2]@ok"

** Lenient mode
83
84
85
   :PROPERTIES:
   :CUSTOM_ID: lenient
   :END:
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

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:

109
#+BEGIN_SRC sh :prologue "exec 2>&1" :epilogue true
110
111
112
113
114
115
ltlfilt -f '(a U b U) U c'
#+END_SRC
#+RESULTS:
: >>> (a U b U) U c
:             ^
: syntax error, unexpected closing parenthesis
116
:
117
118
119
: >>> (a U b U) U c
:            ^
: missing right operand for "until operator"
120
:
121
122
123
124
125
126
127
128
129
130
131
132

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
133
134
135
   :PROPERTIES:
   :CUSTOM_ID: prefix
   :END:
136

137
138
139
140
141
142
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
143

144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
The following operators are supported:

| syntax | meaning        |
|--------+----------------|
|  <c>   | <l>            |
|  =t=   | true           |
|  =f=   | false          |
|  =!=   | not            |
|  =&=   | and            |
| \vert  | or             |
|  =^=   | xor            |
|  =i=   | implies        |
|  =e=   | equivalent     |
|  =X=   | next           |
|  =F=   | eventually     |
|  =G=   | globally       |
|  =U=   | strong until   |
|  =V=   | weak release   |
|  =M=   | strong release |
|  =W=   | weak until     |
|--------+----------------|

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
166
167
As an extension to LBT's syntax, alphanumeric atomic propositions that
follow the "=p= + number" rule will be accepted if they do not
168
conflict with one of the operators (e.g., =i=, the /implies/ operator,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
169
170
cannot be used as an atomic proposition).  Also any atomic proposition
may be double-quoted.  These extensions are compatible with the syntax
171
used by [[http://www.ltl2dstar.de][ltl2dstar]].
172
173
174

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

175

176
* Common output options
177
178
179
   :PROPERTIES:
   :CUSTOM_ID: output-options
   :END:
180
181
182

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

183
#+BEGIN_SRC sh :exports results
184
185
ltlfilt --help | sed -n '/Output options:/,/^$/p' |
  sed '1d;$d;/--.*count/d;/--quiet/d'
186
187
#+END_SRC
#+RESULTS:
188
#+begin_example
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
189
190
  -0, --zero-terminated-output   separate output formulas with \0 instead of \n
                             (for use with xargs -0)
191
  -8, --utf8                 output using UTF-8 characters
192
193
      --format=FORMAT, --stats=FORMAT
                             specify how each line should be output (default:
194
195
196
                             "%f")
  -l, --lbt                  output in LBT's syntax
      --latex                output using LaTeX macros
197
198
199
  -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 '>>'.
200
201
202
203
204
  -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
205

206
The =--spot=, =--utf-8=, =--spin=, =--wring= options select different
207
208
209
210
211
212
213
214
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.
215

216
Note that by default Spot always outputs parentheses around operators
217
218
219
220
221
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=.

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

225
226
227
228
229
230
231
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]].

232
233
234
235
236
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:

237
238
239
240
241
242
|            | =%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 |
243

244
Other =%=-sequences are supported by these tools, and documented in
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
245
246
the output of =--help=.  For instance =%s= can be used to compute the
size of a formula.
247
248

By default everything is output to standard output, so that you can
249
redirect the output to a file, and pipe it to another tool.  The
250
251
252
253
254
255
=--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:

256
#+BEGIN_SRC sh :epilogue "rm -f example-*.ltl"
257
258
259
260
261
262
263
264
265
266
267
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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
268
269
270
271
272
273
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:

274
#+BEGIN_SRC sh
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
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 =-=).


295

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