With the attached system, the liveness checker claims that the property "E
true" is not true. This is obviously not correct.
Created attachment 28 [details]
A fix has been checked into CVS.
The bug made the old implementation an under approximation. I.e. when E p
returned true (or A<> p returned false) this was correct, but when E p
returned false (or A<> p returned true) this might have been wrong.