ioltl.org 6.57 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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
69
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
#+TITLE: Common input and output options for LTL/PSL formulas
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.html

Spot supports different syntaxes for LTL/PSL formulas.  This pages
document 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:

#+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
:   -F, --file=FILENAME        process each line of FILENAME as a formula
:       --lbt-input            read all formulas using LBT's prefix syntax
:       --lenient              parenthesized blocks that cannot be parsed as
:                              subformulas are considered as atomic properties

=-f= is used to pass one formula one 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.

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

These double-quote string 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 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

119
120
121
122
123
124
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
125
126
127
128
129
130

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
131
used by [[http://www.ltl2dstar.de][ltl2dstar]].
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166

=--lbt-input= 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:

#+BEGIN_SRC sh :results verbatim :exports results
ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
:   -8, --utf8                 output using UTF-8 characters
:   -l, --lbt                  output in LBT's syntax
:   -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

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

The =--spot=, =--utf-8=, =--spin=, =--wring= select different
output syntax as seen in [[tab:formula-syntaxes][the above table]].  The =-p= option can
be used to request that parenthesis be used at all levels.

Note that by default Spot always output 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
right-associative in the PSL standard), while Spin (among other tools)
with read it as =(a U b) U c=.

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

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