Bug 327 - Deadlock checker is broken for models with priorities
Summary: Deadlock checker is broken for models with priorities
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Beta 3
Hardware: All All
: P2 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-05-22 20:27 CEST by Gerd Behrmann
Modified: 2006-05-22 20:28 CEST (History)
0 users

See Also:
Architecture:


Attachments
Test case (1.20 KB, text/xml)
2006-05-22 20:27 CEST, Gerd Behrmann
Details
Query file (92 bytes, application/octet-stream)
2006-05-22 20:28 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-22 20:27:27 CEST
The deadlock checker is broken for models with priorties: In the attached model, the result of the verification is wrong (there is a deadlock, but UPPAAL does not find it).
Comment 1 Gerd Behrmann 2006-05-22 20:27:45 CEST
Created attachment 103 [details]
Test case
Comment 2 Gerd Behrmann 2006-05-22 20:28:00 CEST
Created attachment 104 [details]
Query file
Comment 3 Gerd Behrmann 2006-05-22 20:28:18 CEST
Fixed on the trunk from rev. 1833.