Hello, As an alternative, I can suggest you to read this example : https://spot.lrde.epita.fr/ipynb/automata-io.html#Reading-automata-from-stri... Regards, Denis Le 06/11/2020 à 10:10, רועי פוגלר a écrit :
Hello again,
Can you help me please with the previous questions?
I still didn't figure out how to make a specific state as accepting in Buchi automata
Regards, Roi
On Mon, 2 Nov 2020 at 21:03, רועי פוגלר <roi.fogler@gmail.com> wrote:
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@lrde.epita.fr> wrote:
Hi Roi,
On Sat, Oct 31, 2020 at 9:03 PM רועי פוגלר <roi.fogler@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
_______________________________________________ Spot mailing list Spot@lrde.epita.fr https://lists.lrde.epita.fr/listinfo/spot