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