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@lrde.epita.fr> wrote:
>
> On Tue, Nov 10, 2020 at 9:28 PM Philip Schwartz <pschwartz090@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