comapre spot automata
Hello, 1. I tried to compare 2 spot automata as described here -> https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/contai... (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
Hi Roi, On Fri, Oct 30, 2020 at 2:14 PM רועי פוגלר <roi.fogler@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
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@lrde.epita.fr> wrote:
Hi Roi,
On Fri, Oct 30, 2020 at 2:14 PM רועי פוגלר <roi.fogler@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
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
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
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
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
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-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
_______________________________________________ Spot mailing list Spot@lrde.epita.fr https://lists.lrde.epita.fr/listinfo/spot
On Fri, Nov 6, 2020 at 10:11 AM רועי פוגלר <roi.fogler@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
participants (3)
-
Alexandre Duret-Lutz -
Denis Poitrenaud -
רועי פוגלר