allow unabbreviation before converting formulas in ltldo and ltlcross
% ltldo modella -f 'p0 -> p1'
modella: syntax error: p0
error: execution of command "modella 'lcr-i1-hXpGvq' 'lcr-o0-XpHwfQ'" returned exit code 255.
ltldo: aborting here
This is because MoDeLLa uses the LBT syntax but does not support i
(implication) e
(equivalence) or ^
(xor).
We have similar issues with Rabinizer3 that supports U
but not its dual R
. It would be nice if the syntax for specifying translators could support a way to list operators that should be rewritten.
I'm thinking about %[MWie^]L
for MoDeLLa and %[RMW]f
for Rabinizer3. The custom syntax for Python's format()
should support this as well.