compare automata with exclusive_word
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)") print(aut2.exclusive_word(aut)) # actual result - “p2; cycle{p1 & !p2}” # expected - None Best Regards, Phillipp
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
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
On Sat, Nov 14, 2020 at 8:43 PM Philip Schwartz <pschwartz090@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
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@lrde.epita.fr> wrote:
On Sat, Nov 14, 2020 at 8:43 PM Philip Schwartz <pschwartz090@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
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@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@lrde.epita.fr> wrote:
On Sat, Nov 14, 2020 at 8:43 PM Philip Schwartz <pschwartz090@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
On Sun, Nov 15, 2020 at 3:15 PM Philip Schwartz <pschwartz090@gmail.com> wrote:
but it isn't clear to me how to make "1" an accepting state.
You mark all outgoing edges of state 1 as accepting. The link https://spot.lrde.epita.fr/tut22.html#sba that you gave shows how it's done. Especially I thought the first sentence of that section was pretty clear. Can you help me understand what's unclear about it for you, and how we should reformulate it to help future users ? -- Alexandre Duret-Lutz
Hello, I didn't understand how to mark edges as accepting, I thought that it's done by- 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), *[0])* aut.new_edge(1, 1, p2, *[0])* but I see that I still get counterexample using this code: aut2 = spot.translate(spot.formula(*"p1 U p2"*)) bdict = spot.make_bdd_dict() 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.set_buchi() aut.prop_state_acc(True) 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), [0]) aut.new_edge(1, 1, p2, [0]) Regards, Phillipp print(aut2.exclusive_word(aut)) On Mon, 16 Nov 2020 at 09:53, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Sun, Nov 15, 2020 at 3:15 PM Philip Schwartz <pschwartz090@gmail.com> wrote:
but it isn't clear to me how to make "1" an accepting state.
You mark all outgoing edges of state 1 as accepting.
The link https://spot.lrde.epita.fr/tut22.html#sba that you gave shows how it's done. Especially I thought the first sentence of that section was pretty clear. Can you help me understand what's unclear about it for you, and how we should reformulate it to help future users ? -- Alexandre Duret-Lutz
On Mon, Nov 16, 2020 at 8:19 PM Philip Schwartz <pschwartz090@gmail.com> wrote:
I didn't understand how to mark edges as accepting, I thought that it's done by-
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), [0]) aut.new_edge(1, 1, p2, [0])
Yes.
but I see that I still get counterexample using this code:
That's expected: your two automata are not equivalent and print(aut2.exclusive_word(aut)) is showing you why. -- Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
Philip Schwartz