Bug 325 - Wrong results for liveness properties
Summary: Wrong results for liveness properties
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Beta 3
Hardware: All All
: P1 blocker
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-05-10 11:37 CEST by Gerd Behrmann
Modified: 2006-05-10 20:03 CEST (History)
0 users

See Also:
Architecture:


Attachments
Test case in XTA format (287 bytes, application/octet-stream)
2006-05-10 12:30 CEST, Gerd Behrmann
Details
Query file for test case (95 bytes, application/octet-stream)
2006-05-10 12:31 CEST, Gerd Behrmann
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Gerd Behrmann 2006-05-10 11:37:05 CEST
In the attached system, the property 'A<> Process.b' is false. UPPAAL 3.6 claims that it is satisfied. UPPAAL 3.4.11 gives the correct answer.

The problem seems to be in the deadlock check performed by the liveness checker: An optimisation introduced in 3.6 has the effect that the target invariant in some cases is ignored.
Comment 1 Gerd Behrmann 2006-05-10 12:30:57 CEST
Created attachment 101 [details]
Test case in XTA format
Comment 2 Gerd Behrmann 2006-05-10 12:31:11 CEST
Created attachment 102 [details]
Query file for test case
Comment 3 Gerd Behrmann 2006-05-10 20:03:24 CEST
Fixed on the trunk from rev. 1799.