12 Nov
2020
12 Nov
'20
9 a.m.
Hello Prof. Alexandre Duret-Lutz,
Thank you again for the detailed answers,
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')
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.
Regards,
Phillipp
On Wed, 11 Nov 2020 at 21:10, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
On Wed, Nov 11, 2020 at 2:38 PM Philip Schwartz <pschwartz090(a)gmail.com> wrote:
I read my previous email and I thought maybe I
was not clear enough:
My problem is transferring the "until" operator to an action recognized by spot
(such as ! ).
That's making it even more confusing.
Spot only supports automa labelled by Boolean formulas over atomic propositions.
If you really expect to label an edge by an LTL formula, can you
describe the semantic of such an edge ?
--
Alexandre Duret-Lutz 