On Thu, Nov 12, 2020 at 9:00 AM Philip Schwartz pschwartz090@gmail.com wrote:
My point is that I want to copy the behavior of the tool presented in the attached picture (just typed p1Up2&p2 here - https://spot.lrde.epita.fr/app/ and got automata with 2 states and the label of the edge form "1" to "0" is 'p1Up2&p2')
Please check the output difference between typing "(p1 U p2) & p2" and "p1Up2 & p2". p1Up2 is just an arbitrary name that is assumed to be an atomic proposition.
The difference between "aUb", and "a U b" is also discussed in the help text (Help > LTL Infix Syntax > Atomic Propositions) for the online tool,
I'm trying to do the same using "Creating an automaton by adding states and transitions" as described in this guideline - https://spot.lrde.epita.fr/tut22.html.
This page uses two AP named "p1" and "p2". You can name them as you want by changing the argument of register_ap().