12 Nov
2020
12 Nov
'20
9:22 a.m.
On Thu, Nov 12, 2020 at 9:00 AM Philip Schwartz <pschwartz090(a)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().
--
Alexandre Duret-Lutz