Bug 59 - missing report of a cycle while checking a E[] property
Summary: missing report of a cycle while checking a E[] property
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.0
Hardware: All All
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2003-09-16 16:10 CEST by Arne Skou
Modified: 2006-09-10 11:43 CEST (History)
0 users

See Also:
Architecture:


Attachments
model used at bug 59 report (22.20 KB, application/octet-stream)
2003-09-16 16:12 CEST, Arne Skou
Details
property checked at bug 59 (145 bytes, text/plain)
2003-09-16 16:13 CEST, Arne Skou
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Arne Skou 2003-09-16 16:10:31 CEST
The model checker does not report an infinite cycle with read marking when
checking a specific model for a E[] property
Comment 1 Arne Skou 2003-09-16 16:12:00 CEST
Created attachment 5 [details]
model used at bug 59 report
Comment 2 Arne Skou 2003-09-16 16:13:41 CEST
Created attachment 6 [details]
property checked at bug 59
Comment 3 Gerd Behrmann 2003-09-16 19:01:31 CEST
UPPAAL is detecting a deadlock in the system, which does not exist. This is
caused by a bug in the microDelay() method, which causes the internal DBM
representation to contain invalid entries, thus destroying the information about
the zone of the state. A fix was checked into CVS yesterday.

I talked to Paul today, and we agreed to release version 3.4.1 at the end of the
week.