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