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

Bug 384 - Wrong result in liveness check
Summary: Wrong result in liveness check
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.3
Hardware: All All
: P2 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-12-21 17:14 CET by Gerd Behrmann
Modified: 2006-12-22 10:37 CET (History)
0 users

See Also:
Architecture:

Attachments
Test case (3.88 KB, text/xml)
2006-12-21 17:15 CET, Gerd Behrmann 		Details
Query file (43 bytes, application/octet-stream)
2006-12-21 17:15 CET, Gerd Behrmann 		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 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.