From 1f4e035147f77158be01a4d2f5f87a79865a9ac1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Mar 2013 16:43:32 +0100 Subject: [PATCH] * doc/org/ioltl.org: Fix link to ltl2dstar. --- doc/org/ioltl.org | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 597752d5a..c65f07ed9 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -116,19 +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]], [[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. +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 [[www.ltl2dstar.de][ltl2dstar]]. +used by [[http://www.ltl2dstar.de][ltl2dstar]]. =--lbt-input= is a global option that affects *all* formulas that are read.