alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: update for 1.0.1

Browse source 
* doc/org/ioltl.org: Mention ltl2dstar and the changes to the prefix
parser.
* doc/org/ltlcross.org: Mention bench/ltl2tgba/sum.py.
* doc/org/tools.org: Bump version number.
This commit is contained in:
Alexandre Duret-Lutz 2013-01-23 18:31:54 +01:00
parent 152a46b961
commit d1ad744887
3 changed files with 15 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

20
doc/org/ioltl.org
View file

@ -116,15 +116,19 @@ 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.
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
[[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, atomic propositions may also be
double-quoted. In that case they do not have to follow the "=p= +
number" rule.
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 [[www.ltl2dstar.de][ltl2dstar]].
=--lbt-input= is a global option that affects *all* formulas that are read.

2
doc/org/ltlcross.org
View file

@ -252,6 +252,8 @@ for i in range(0, len(data["tools"])):
: spin -f %s >%N & 4 & 4.50 & 11.25 & 25.00 & 1.00 & 2.75 & 3.50 & 1.00 & 0.01 & 848.25 & 24779.75 & 3.25 \\
: lbt < %L >%T & 4 & 15.75 & 88.75 & 183.50 & 1.75 & 11.50 & 12.75 & 1.00 & 0.00 & 2660.75 & 169623.50 & 1218.50 \\
The script =bench/ltl2tgba/sum.py= is a more evolved version of the
above script that generates two kinds of LaTeX tables.
When computing such statistics, you should be aware that inputs for
which a tool failed to generate an automaton (e.g. it crashed, or it

2
doc/org/tools.org
View file

@ -1,4 +1,4 @@
#+TITLE: Command-line tools installed by Spot 1.0
#+TITLE: Command-line tools installed by Spot 1.0.1
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t