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: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: normal    
Priority: P2    
Version: 3.4.0   
Hardware: All   
OS: All   
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