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

Bug 384

Summary: Wrong result in liveness check
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: major    
Priority: P2    
Version: 4.0.3   
Hardware: All   
OS: All   
Architecture:
Attachments: Test case
Query file

Description Gerd Behrmann 2006-12-21 17:14:31 CET 
Submitted by Daniel Karlsson on the public mailing list:

I've used the attached traffic light problem as an example in a course
for some years now. It has always worked for the Uppaal 3 versions, but
now as I wanted (had to) upgrade to version 4 some properties failed. I
have investigated the diagnostic trace, but I can't understand why they
fail.

Might there be a bug in the new version, or perhaps there has always
been a bug in my model which completely escapes me?
Comment 1 Gerd Behrmann 2006-12-21 17:15:18 CET 
Created attachment 132 [details]
Test case
Comment 2 Gerd Behrmann 2006-12-21 17:15:37 CET 
Created attachment 133 [details]
Query file
Comment 3 Gerd Behrmann 2006-12-22 10:29:20 CET 
Fixed on the 4.0 branch from rev. 2872.
Comment 4 Gerd Behrmann 2006-12-22 10:37:00 CET 
Fixed on the trunk from rev. 2874.