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

Bug 324

Summary:	Wrong result when using conjunction with deadlock property
Product:	UPPAAL	Reporter:	Gerd Behrmann <behrmann>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	critical
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-09 09:49:27 CEST

In the attached model, the property 'E<> deadlock and x < 2' is not satisfied. However, UPPAAL claims it is. Upon generating a witnessing trace, UPPAAL crashes.

Comment 1 Gerd Behrmann 2006-05-09 09:49:54 CEST

Created attachment 99 [details]
Test case in XTA format

Comment 2 Gerd Behrmann 2006-05-09 09:50:33 CEST

Created attachment 100 [details]
Query file for test case

Comment 3 Gerd Behrmann 2006-05-09 11:39:47 CEST

This is also a bug in 3.4.11.

Comment 4 Gerd Behrmann 2006-05-09 21:21:16 CEST

Fixed on the trunk from rev. 1795.