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

Bug 333

Summary:	Leads-to property check inconsistent with different trace options
Product:	UPPAAL	Reporter:	Marius Mikučionis <marius>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	normal
Priority:	P2
Version:	4.0.1
Hardware:	All
OS:	All
Architecture:
Attachments:	sample spec to demonstrate bug

Description Marius Mikučionis 2006-07-07 11:05:44 CEST

consider system of two processes:

chan io;

p1:
s1 --io!--> s2 ----> s3

p2:
s1 --io?--> s2 ----> s3

go to verifier, ask to verify property (p1.s1 --> p2.s2):
1) verifier says property is not satisfied when diagnostic trace is none or some
2) verifier says property is satisfied when diagnostic trace is shortest or fastest

Comment 1 Marius Mikučionis 2006-07-07 11:10:08 CEST

Created attachment 105 [details]
sample spec to demonstrate bug

Comment 2 Gerd Behrmann 2006-07-08 13:05:59 CEST

Generating shortest and fastest traces for any liveness property is not supported. This should be documented and an error should be generated for this particular case.

Comment 3 Gerd Behrmann 2006-07-13 10:22:27 CEST

*** Bug 339 has been marked as a duplicate of this bug. ***

Comment 4 Gerd Behrmann 2006-07-31 20:29:00 CEST

The inconsistency was caused by a wrong initialisation of the pruning threshold in the PassedWaitingList implementations. This is fixed on the 4.0 branch from rev. 2480. The trunk was already fixed.

Shortest and fastest trace settings stil have no effect on liveness properties (the traces with neither be shortest nor fastest), however the result should be correct.