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

* doc/org/ioltl.org: Fix link to ltl2dstar.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-03-20 16:43:32 +01:00
parent e23203b819
commit 1f4e035147
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
doc/org/ioltl.org
View file

@ -116,19 +116,19 @@ Here =a U b U= was taken as an atomic proposition.
** Prefix parser ** 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 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]]
[[www.ltl2dstar.de][ltl2dstar]] requires a different parser. For these tools, the above requires a different parser. For these tools, the above example
example formula has to be written =G i p0 V p1 ! p2= (in LBT's syntax, formula has to be written =G i p0 V p1 ! p2= (in LBT's syntax, atomic
atomic propositions must start with =p= and be followed by a number). propositions must start with =p= and be followed by a number). Spot's
Spot's =--lbt-input= option can be used to activate the parser for =--lbt-input= option can be used to activate the parser for this
this syntax. syntax.
As an extension to LBT's syntax, alphanumeric atomic propositions that As an extension to LBT's syntax, alphanumeric atomic propositions that
follow the "=p= + number" rule will be accepted if they do not follow the "=p= + number" rule will be accepted if they do not
conflict with one of the operator (e.g., =i=, the implies operator, conflict with one of the operator (e.g., =i=, the implies operator,
cannot be used as an atomic proposition). Also any atomic proposition cannot be used as an atomic proposition). Also any atomic proposition
may be double-quoted. These extensions are compatible with the syntax 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. =--lbt-input= is a global option that affects *all* formulas that are read.