Bug 140 - Liveness checker gives wrong answer
Summary: Liveness checker gives wrong answer
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.8
Hardware: All All
: P5 blocker
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-03-29 18:00 CEST by Gerd Behrmann
Modified: 2005-06-29 21:29 CEST (History)
0 users

See Also:
Architecture:


Attachments
Test case (1.54 KB, application/octet-stream)
2005-03-29 18:01 CEST, Gerd Behrmann
Details

Note You need to log in before you can comment on or make changes to this bug.
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.