2 Nov
2020
2 Nov
'20
11:23 a.m.
Hi Roi,
On Sat, Oct 31, 2020 at 9:03 PM רועי פוגלר <roi.fogler(a)gmail.com> wrote:
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}.
No, your second automaton (aut) accepts every word because the default
acceptance condition is "true" and you have commented the call to
aut.set_buchi().
run = self.s.exclusive_run(aut)
if not run:
return True, ''
else:
counterexample = str(spot.make_twa_word(run))
return False, counterexample
You might as well call s.exclusive_word(aut) directly if you want a word.
--
Alexandre Duret-Lutz