[Spot] compare automata with exclusive_word

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