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@lrde.epita.fr wrote:
On Sat, Nov 14, 2020 at 7:23 PM Philip Schwartz pschwartz090@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