30 Oct
2020
30 Oct
'20
2:13 p.m.
Hello,
1. I tried to compare 2 spot automata as described here ->
https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/conta…
(last section)
but, I got a counterexample which I think is not correct since both
automata are not accepting this counterexample:
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.
2. Is there a way to transfer spot automata to LTL?
Regards,
Roi
30 Oct
30 Oct
2:33 p.m.
Hi Roi,
On Fri, Oct 30, 2020 at 2:14 PM רועי פוגלר <roi.fogler(a)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.
2. Is there a way to transfer spot automata to LTL?
No.
--
Alexandre Duret-Lutz
31 Oct
31 Oct
9:02 p.m.
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(a)lrde.epita.fr>
wrote:
Hi Roi,
On Fri, Oct 30, 2020 at 2:14 PM רועי פוגלר <roi.fogler(a)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.
2. Is there a way to transfer spot automata to
LTL?
No.
--
Alexandre Duret-Lutz
2 Nov
2 Nov
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
8:03 p.m.
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
6 Nov
6 Nov
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
10:21 a.m.
Hello,
As an alternative, I can suggest you to read this example :
https://spot.lrde.epita.fr/ipynb/automata-io.html#Reading-automata-from-str…
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(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
_______________________________________________
Spot mailing list
Spot(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot
12:44 p.m.
Re,
You can also have a look at :
https://gitlab.lrde.epita.fr/spot/spot/-/blob/next/doc/org/tut22.org
D.
Le 06/11/2020 à 10:21, Denis Poitrenaud a écrit :
Hello,
As an alternative, I can suggest you to read this example :
https://spot.lrde.epita.fr/ipynb/automata-io.html#Reading-automata-from-str…
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(a)gmail.com>
wrote:
_______________________________________________
Spot mailing list
Spot(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot
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
_______________________________________________
Spot mailing list
Spot(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot
8 Nov
8 Nov
11:06 a.m.
On Fri, Nov 6, 2020 at 10:11 AM רועי פוגלר <roi.fogler(a)gmail.com> wrote:
I still didn't figure out how to make a specific
state as accepting in
Buchi automata
You simply mark all the outgoing transitions of this state as
accepting, as in the tut22 page mentioned several times already.
--
Alexandre Duret-Lutz
1550
days inactive
1559
days old
8 comments
3 participants
participants (3)
-
Alexandre Duret-Lutz -
Denis Poitrenaud -
רועי פוגלר