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

Bug 325

Summary: Wrong results for liveness properties
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Severity: blocker    
Priority: P1    
Version: 3.6 Beta 3   
Hardware: All   
OS: All   
Attachments: Test case in XTA format
Query file for test case

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.