|Summary:||Liveness checker gives wrong answer|
|Product:||UPPAAL||Reporter:||Gerd Behrmann <behrmann>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
Description Gerd Behrmann 2005-03-29 18:00:39 CEST
With the attached system, the liveness checker claims that the property "E true" is not true. This is obviously not correct.
Comment 2 Gerd Behrmann 2005-03-29 20:16:23 CEST
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.