30 Oct
2020
30 Oct
'20
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