9 Nov
2020
9 Nov
'20
9:05 a.m.
On Sun, Nov 8, 2020 at 10:20 PM Philip Schwartz <pschwartz090(a)gmail.com> wrote:
In addition, when trying to translate a
"concatenation" I get error message: "unexpected atomic proposition"
E.g. spot.formula("p2;p1&!p2").translate()
Concatenation is only valid in Semi-Extended Regular Expressions
(SERE), and those recognize finite words.
As Spot deals with LTL or PSL formulas over infinite words, you need
to select how to interpret your SERE over finite words by including it
into one of {...} or {...}!
In your simple example there is no difference between "{p2;p1&!p2}" or
"{p2;p1&!p2}!", they are both equivalent to the LTL formula "p2 &
X(p1
& !p2)".
See https://spot.lrde.epita.fr/tl.pdf section 2.6 for the
specification of {r} and {r}! (the latter being syntactic sugar for
{r}<>->1).
--
Alexandre Duret-Lutz