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