Hello,
After changing to set_acceptance(1, "Inf(0)") it still returns “p2;
cycle{p1 & !p2}”,
I thought that after "set_acceptance(1, "Inf(0)")" it makes
"1" as
accepting state so why the automata accepts only empty language?
Regards,
Phillipp
On Sat, 14 Nov 2020 at 21:31, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
On Sat, Nov 14, 2020 at 7:23 PM Philip Schwartz <pschwartz090(a)gmail.com> wrote:
Hello Prof. Alexandre Duret-Lutz
Thank you again for all your answers.
I tried to compare 2 automats created using spot and got a a
counterexample although
they seems to be equal:
aut2 = spot.translate(spot.formula("p1 U p2"))
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)
aut.set_acceptance(1, "Inf(1)")
If you declare one color, the color should not be higher than 0.
Probably you meant set_acceptance(1, "Inf(0)").
Anyway, since no edge of aut is accepting, the entire automaton
recognizes the empty language (unlike aut2).
--
Alexandre Duret-Lutz