spot/doc/org/ioltl.org

#+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]], or [[http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/][scheck]], require
a different parser.  For these tools, the above example formula has to
be written =G i p0 V p1 ! p2= (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, atomic propositions may also be
double-quoted.  In that case they do not have to follow the "=p= +
number" rule.

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