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

Bug 325

Summary:	Wrong results for liveness properties
Product:	UPPAAL	Reporter:	Gerd Behrmann <behrmann>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	blocker
Priority:	P1
Version:	3.6 Beta 3
Hardware:	All
OS:	All
Architecture:
Attachments:	Test case in XTA format Query file for test case

Description Gerd Behrmann 2006-05-10 11:37:05 CEST

In the attached system, the property 'A<> Process.b' is false. UPPAAL 3.6 claims that it is satisfied. UPPAAL 3.4.11 gives the correct answer.

The problem seems to be in the deadlock check performed by the liveness checker: An optimisation introduced in 3.6 has the effect that the target invariant in some cases is ignored.

Comment 1 Gerd Behrmann 2006-05-10 12:30:57 CEST

Created attachment 101 [details]
Test case in XTA format

Comment 2 Gerd Behrmann 2006-05-10 12:31:11 CEST

Created attachment 102 [details]
Query file for test case

Comment 3 Gerd Behrmann 2006-05-10 20:03:24 CEST

Fixed on the trunk from rev. 1799.