30 Jul
2020
30 Jul
'20
4:56 p.m.
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
31 Jul
31 Jul
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
1650
days inactive
1651
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Niklas Metzger