From d1ad744887d344064f8cf1d2fe7f1292ac9ad680 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Jan 2013 18:31:54 +0100 Subject: [PATCH] org: update for 1.0.1 * 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. --- doc/org/ioltl.org | 20 ++++++++++++-------- doc/org/ltlcross.org | 2 ++ doc/org/tools.org | 2 +- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index df637739f..597752d5a 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -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. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index c59efc054..ebfffc59f 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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 diff --git a/doc/org/tools.org b/doc/org/tools.org index 41e51811b..b05dd1088 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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