[Spot] 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