1. I tried to compare 2 spot automata as described here -> https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/contains.ipynb

(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