Re: [Spot] compare automata with exclusive_word

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.