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).
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 ?
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 -
Philip Schwartz