14 Nov
2020
14 Nov
'20
7:23 p.m.
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
14 Nov
14 Nov
8:30 p.m.
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
8:43 p.m.
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
9:12 p.m.
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
9:39 p.m.
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
15 Nov
15 Nov
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
16 Nov
16 Nov
8:52 a.m.
On Sun, Nov 15, 2020 at 3:15 PM Philip Schwartz <pschwartz090(a)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
8:18 p.m.
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(a)lrde.epita.fr>
wrote:
On Sun, Nov 15, 2020 at 3:15 PM Philip Schwartz
<pschwartz090(a)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
8:33 p.m.
On Mon, Nov 16, 2020 at 8:19 PM Philip Schwartz <pschwartz090(a)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
1577
days inactive
1579
days old
8 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Philip Schwartz