Bug 323 - Wrong result with E<> not deadlock property.
Summary: Wrong result with E<> not deadlock property.
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Beta 3
Hardware: All All
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-05-08 19:31 CEST by Gerd Behrmann
Modified: 2006-05-08 23:20 CEST (History)
0 users

See Also:
Architecture:


Attachments
Test case in XTA format (296 bytes, application/octet-stream)
2006-05-08 19:38 CEST, Gerd Behrmann
Details
Query file for test case (95 bytes, application/octet-stream)
2006-05-08 19:38 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-08 19:31:53 CEST
In the attached system, the property E<> not deadlock is satisfied (the initial state is not deadlocked). However, UPPAAL states that this property is not satisfied. The normal case of E<> deadlock or A[] not deadlock is not affected.

Normally, I clasify wrong verification results as critical, however the practical use of such a property is limitted.
Comment 1 Gerd Behrmann 2006-05-08 19:32:41 CEST
BTW: This also affects 3.4.11.
Comment 2 Gerd Behrmann 2006-05-08 19:38:24 CEST
Created attachment 97 [details]
Test case in XTA format
Comment 3 Gerd Behrmann 2006-05-08 19:38:43 CEST
Created attachment 98 [details]
Query file for test case
Comment 4 Gerd Behrmann 2006-05-08 23:20:09 CEST
Fixed on the trunk from rev. 1790.