15 Nov
2020
15 Nov
'20
3:15 p.m.
Hello,
I really appreciate if you can fix my code how can I set the "1" state
as accepting state so the automata will satisfy the "p1 U p2" formula:
aut = spot.make_twa_graph(aut2.get_dict())
p1 = buddy.bdd_ithvar(aut.register_ap("p1"))
p2 = buddy.bdd_ithvar(aut.register_ap("p2"))
aut.new_states(2)
aut.set_init_state(0)
aut.new_edge(0, 0, p1 & buddy.bdd_not(p2))
aut.new_edge(0, 1, p2)
aut.new_edge(1, 1, p1 & buddy.bdd_not(p2))
aut.new_edge(1, 1, p2)
I saw in the guideline that you use
aut.set_buchi()
aut.prop_state_acc(True)
but it isn't clear to me how to make "1" an accepting state.
Regards,
Phillipp
On Sat, 14 Nov 2020 at 20:39, Philip Schwartz <pschwartz090(a)gmail.com> wrote:
Hello,
Actually I see that I didn't understand well the explanation about
setting acceptance condition to buchi automata
(https://spot.lrde.epita.fr/tut22.html#sba):
After these two commands,
aut.set_buchi()
aut.prop_state_acc(True)
How can I make a state accepting?
e.g. in the previous example, how I set the "1" state as accepting?
Thank you for your time and answers
Phillipp
On Sat, 14 Nov 2020 at 22:13, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
>
> On Sat, Nov 14, 2020 at 8:43 PM Philip Schwartz <pschwartz090(a)gmail.com>
wrote:
> > After changing to set_acceptance(1, "Inf(0)") it still returns “p2;
> > cycle{p1 & !p2}”,
>
> That's because the second paragraph of my previous answer still holds...
>
> > I thought that after "set_acceptance(1, "Inf(0)")" it makes
"1" as
> > accepting state so why the automata accepts only empty language?
>
> What made you think that?
> --
> Alexandre Duret-Lutz