Hi Spot Team!
First of all, thanks for providing and maintaining such a great tool! 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. Is there a technical reason for that and if not, could you give me a hint how to implement it?
Thanks in advance Niklas Metzger
Hi Niklas,
On Fri, Jul 31, 2020 at 8:04 AM Niklas Metzger niklas.metzger@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
-
Alexandre Duret-Lutz -
Niklas Metzger