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

Bug 333 - Leads-to property check inconsistent with different trace options
Summary: Leads-to property check inconsistent with different trace options
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.1
Hardware: All All
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-07-07 11:05 CEST by Marius Mikučionis
Modified: 2006-07-31 20:29 CEST (History)
0 users

See Also:
Architecture:

Attachments
sample spec to demonstrate bug (1.22 KB, application/xml)
2006-07-07 11:10 CEST, Marius Mikučionis 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this 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.