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

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
Add an attachment (proposed patch, testcase, etc.)

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.