Re: [Spot] comapre spot automata

Thank you for your help. In case my automata is a buchi automata and I use "aut.set_buchi()". 1. How can I make only a specific state to accept? 2. How I leave the automata as a non accepting automata Regards, Roi On Mon, 2 Nov 2020 at 12:23, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote: > > 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