11 Nov
2020
11 Nov
'20
2:38 p.m.
Hello again,
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 ! ).
Regards,
Phillipp
On Tue, Nov 10, 2020, 23:49 Philip Schwartz <pschwartz090(a)gmail.com> wrote:
Hello,
Thank you for your answer, I still didn't understand, in case the
action is "p1Up2&p2".
How can I pass this as parameter to new edge function?
Regards
Phillipp
On Tue, 10 Nov 2020 at 23:42, Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
On Tue, Nov 10, 2020 at 9:28 PM Philip Schwartz <pschwartz090(a)gmail.com>
wrote:
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
There is no support for "actions", "events", or arbitrary
"letters" in
Spot's automata.
The only kind of "letters" we support are assignments of a set of
predeclared atomic propositions.
If you have a set of predefined actions like "eat", "walk",
"sleep",
you could use some atomic propositions to binary encode them.
For instance:
"eat" = !p0 & !p1
"walk" = !p0 & p1
"sleep" = p0 & !p1
Then work with that. Spot will only want to hear about those p0, p1
propositions, so the mapping (and naming of the propositions) is up to
you.
An alternative encoding, that is more expensive in number of atomic
propositions, but easier to work with for us humans is
"eat" = eat & !walk & !sleep
"walk" = !eat & walk & !sleep
"sleep" = !eat & !walk & sleep
(See also http://lists.lrde.epita.fr/pipermail/spot/2020q3/000293.html
for an answer to a related question.)
--
Alexandre Duret-Lutz