consider system of two processes:
s1 --io!--> s2 ----> s3
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
Created attachment 105 [details]
sample spec to demonstrate bug
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.
*** Bug 339 has been marked as a duplicate of this bug. ***
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.