This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 140

Summary: Liveness checker gives wrong answer
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: blocker    
Priority: P5    
Version: 3.4.8   
Hardware: All   
OS: All   
Attachments: Test case

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 1 Gerd Behrmann 2005-03-29 18:01:09 CEST
Created attachment 28 [details]
Test case
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.