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

Bug 140

Summary:	Liveness checker gives wrong answer
Product:	UPPAAL	Reporter:	Gerd Behrmann <behrmann>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	CLOSED FIXED
Severity:	blocker
Priority:	P5
Version:	3.4.8
Hardware:	All
OS:	All
Architecture:
Attachments:	Test case

Description Gerd Behrmann 2005-03-29 18:00:39 CEST

With the attached system, the liveness checker claims that the property "E[]
true" is not true. This is obviously not correct.

Comment 1 Gerd Behrmann 2005-03-29 18:01:09 CEST

Created attachment 28 [details]
Test case

Comment 2 Gerd Behrmann 2005-03-29 20:16:23 CEST

A fix has been checked into CVS. 

The bug made the old implementation an under approximation. I.e. when E[] p
returned true (or A<> p returned false) this was correct, but when E[] p
returned false (or A<> p returned true) this might have been wrong.