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

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.