The first automata represents the ltl formula p1Up2 so it shouldn't accept cycle{P1 & !p2}.
The second automata is a naive automata with only one not-accepting state, so it shouldn't accept anything, in particular cycle{P1 & !p2}.
code example for the above:
self.s = spot.translate(spot.formula('p1 U p2'))bdict = self.s.get_dict()
aut = spot.make_twa_graph(bdict)
# temporary we will use p1 and p2 only
p1 = spot.buddy.bdd_ithvar(aut.register_ap("p1"))
p2 = spot.buddy.bdd_ithvar(aut.register_ap("p2"))
# Set the acceptance condition of the automaton to Inf(0)
# aut.set_buchi()
# Pretend this is state-based acceptance
aut.prop_state_acc(True)
# States are numbered from 0.
aut.new_states(1)
# The default initial state is 0, but it is always better to
# specify it explicitly.
aut.set_init_state(int(0))
aut.new_edge(int(0), int(0), spot.buddy.bddtrue)
aut.new_edge(int(0), int(0), p2)
run = self.s.exclusive_run(aut)
if not run:
return True, ''
else:
counterexample = str(spot.make_twa_word(run))
return False, counterexample