ioltl.org 10.8 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: Common input and output options for LTL/PSL formulas
3
4
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
5

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

27
=-f= is used to pass one formula on the command line, but this option can
28
29
30
31
32
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
33
34
35
36
37
38
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]].
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

** 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58
59
operators, please refer to the
[[https://spot.lrde.epita.fr/tl.pdf][=doc/tl/tl.pdf= document inside the Spot distribution]].
60
61
62
63
64
65
66
67
68
69

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

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

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

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

143

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

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

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

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

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

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

201
202
203
204
205
|           | =%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)       |
206

207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232

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 the
=--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

#+BEGIN_SRC sh :results verbatim :exports none
rm -f example-*.ltl
#+END_SRC
#+RESULTS:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
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 =-=).


260

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