Hello,
I'll try to be more specific:
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
Regards, Roi
On Fri, 30 Oct 2020 at 15:33, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
Hi Roi,
On Fri, Oct 30, 2020 at 2:14 PM רועי פוגלר roi.fogler@gmail.com wrote:
I tried to compare automata which presents P1 U p2 and automata which
answers
"no" to everything and I got cycle{P1 & !p2} as a counterexample. attached picture with the code and examples from Ide.
This code does not show the two automatas and their acceptance condition, so there is no way I can reproduce the problem. For what I can tell, if the displayed automaton has "true" acceptance, it accepts any word, including cycle{P1 & !p2}. Also it does not mention P1, so I have no clue what the formula "P1 U p2" is referring to in your email.
- Is there a way to transfer spot automata to LTL?
No.
Alexandre Duret-Lutz