30 Oct
2020
30 Oct
'20
2:13 p.m.
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
