On Sun, Nov 8, 2020 at 10:20 PM Philip Schwartz pschwartz090@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).