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

Bug 59

Summary:	missing report of a cycle while checking a E[] property
Product:	UPPAAL	Reporter:	Arne Skou <ask>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	CLOSED FIXED
Severity:	normal
Priority:	P2
Version:	3.4.0
Hardware:	All
OS:	All
Architecture:
Attachments:	model used at bug 59 report property checked at bug 59

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.