Thank you again for the detailed explanation.
When adding edges using "aut.new_edge" as in this example https://spot.lrde.epita.fr/tut22.html how can I transfer a string to bdd for the third parameter? e.g. in case the action is "p1Up2&p2" and I want to add it as edge
aut.new_edge(1, 2, "p1Up2&p2".to_bdd())
Best Regards,
Phillipp
On Mon, 9 Nov 2020 at 10:05, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
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).
-- Alexandre Duret-Lutz