166 lines
6.6 KiB
Org Mode
166 lines
6.6 KiB
Org Mode
#+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
|
|
|
|
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.
|
|
|
|
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
|
|
used by [[http://www.ltl2dstar.de][ltl2dstar]].
|
|
|
|
=--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
|