Re: [Spot] comapre spot automata

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.