|Summary:||Leads-to property check inconsistent with different trace options|
|Product:||UPPAAL||Reporter:||Marius Mikučionis <marius>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
|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.