|Summary:||Wrong result in liveness check|
|Product:||UPPAAL||Reporter:||Gerd Behrmann <behrmann>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
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 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.