31 Jul
2020
31 Jul
'20
9:50 a.m.
Hi Niklas,
On Fri, Jul 31, 2020 at 8:04 AM Niklas Metzger
<niklas.metzger(a)cispa.saarland> wrote:
I stumbled over a problem with formulas in polish
notation: Parsing a formula like “-> a b” returns the “syntax error, unexpected
implication operator” (Also tested on the website). It seems like implication and
equivalence are not supported by that parser.
They are, but not with this syntax. The prefix syntax we support is
compatible with the ones used by tools such as lbt, lbtt, scheck,
ltl2dstar, in which all operators are single letters. Implication is
"i", equivalence is "e".
It seems the only documentation about this syntax we have in Spot are
links to the aforementioned tools, so I'll change
https://spot.lrde.epita.fr/ioltl.html#org4f2e98e to list those
operators in the next release.
At least the help text for https://spot.lrde.epita.fr/app/
(technically not part of the Spot distribution) makes it clear that
those operators are "i" and "e".
If you know of some actual tool that supports a different prefix
syntax, maybe with "->" and "<->" instead of "i"
and "e", please let
us know. Adding support for "->" and "<->" in addition to
"i" and "e"
would be trivial but I see no point in doing so unless it's an
established practice.
Alexandre