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

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
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 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.