6 Nov
2020
6 Nov
'20
10:10 a.m.
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(a)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(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