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

Bug 323

Summary:	Wrong result with E<> not deadlock property.
Product:	UPPAAL	Reporter:	Gerd Behrmann <behrmann>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	normal
Priority:	P2
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-08 19:31:53 CEST

In the attached system, the property E<> not deadlock is satisfied (the initial state is not deadlocked). However, UPPAAL states that this property is not satisfied. The normal case of E<> deadlock or A[] not deadlock is not affected.

Normally, I clasify wrong verification results as critical, however the practical use of such a property is limitted.

Comment 1 Gerd Behrmann 2006-05-08 19:32:41 CEST

BTW: This also affects 3.4.11.

Comment 2 Gerd Behrmann 2006-05-08 19:38:24 CEST

Created attachment 97 [details]
Test case in XTA format

Comment 3 Gerd Behrmann 2006-05-08 19:38:43 CEST

Created attachment 98 [details]
Query file for test case

Comment 4 Gerd Behrmann 2006-05-08 23:20:09 CEST

Fixed on the trunk from rev. 1790.