Bug 222 - Fastest trace error
Summary: Fastest trace error
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 1
Hardware: All All
: P2 minor
Assignee: Gerd Behrmann
URL: http://mark.pavlidis.org/code/uppaal/
Depends on:
Reported: 2005-11-10 22:18 CET by Mark Pavlidis
Modified: 2006-01-03 16:25 CET (History)
0 users

See Also:

Test case system (2.07 KB, application/xml)
2005-11-11 04:20 CET, Mark Pavlidis
Test case query (103 bytes, application/octet-stream)
2005-11-11 04:23 CET, Mark Pavlidis

Note You need to log in before you can comment on or make changes to this bug.
Description Mark Pavlidis 2005-11-10 22:18:59 CET
I am attempting to use UPPAAL (3.6a1) to find the fastest trace through a TA.  Using the system and 
query found at http://mark.pavlidis.org/code/uppaal/ and model checking with Options->Diagnostic 
Trace->Fastest, it produces an error "Bad file descriptor" and "Server connection lost" (on OS X).  On 
Linux, it further reports "CAUGHT EXECPTION: Cannot use LU extrapolation for this property".

I have tried all the possible setting of the other options along with Diagnosic Trace->Fastest, and the 
errors for all combinations.  

The error does not with Trace->Shortest selected.

This problem also occurs with v.3.5.7, but not with 3.4.11.  The latter nicely produces a fastest trace 
for "A[] not deadlock". 

As an aside, the documentation indicates that it "generates a trace (if there is one) that shows how the 
checked property is (or is not) satisfied."  It appears as though I can only get it to load a trace if the 
checked property is not satisfied.  Please update the documentation, or contact me directly I am 
improperly using the tool.
Comment 1 Mark Pavlidis 2005-11-11 04:20:03 CET
Created attachment 68 [details]
Test case system

This is the system that produces the error when generating the fastest trace.
Comment 2 Mark Pavlidis 2005-11-11 04:23:16 CET
Created attachment 69 [details]
Test case query

Query used to cause the error.
Comment 3 Gerd Behrmann 2005-11-14 17:33:02 CET
UPPAAL cannot find fastest traces to deadlocks. The fastest trace feature relies
on using a specific extrapolation operation (the "LU extrapolation" - a new kind
of abstraction introduced in version 3.6), but deadlocks are not preserved by
this  abstraction. Therefore, in order to find deadlocks, UPPAAL does not use
this extrapolation operation - however this implies that it cannot find fastest
traces when searching for deadlocks. UPPAAL 3.4 used an entirely different
approach to finding fastest traces. I will consider if we can do anything about
this issue. We will at least update the documentation and make sure that the GUI
produces a better error message.

Is it essential to be able to find the fastest trace to a deadlock - could it be
rephrased to location reachability? 

As for documentation on the generation of traces, the point is that UPPAAL will
generate a trace if there is a trace. If an A[] property is satisfied, then
there is no trace. On the other hand if an E<> property is satisfied, then there
is a trace. So from a technical point of view, the documentation is correct. But
I see that it is misleading and should be rephrased.
Comment 4 Mark Pavlidis 2005-12-19 05:00:31 CET
I automatically generate the TA.  The trace to deadlock was the easiest way I found to obtain the fastest 
trace (with 3.4) since the model is known to have a single terminating location.  I have reworked the 
generation of the TA to ID the terminating location and rephrased the query to location reachability, as 
you suggested.  This solves the issue I had, and is a cleaner solution than finding deadlocks.
Comment 5 Gerd Behrmann 2006-01-03 16:25:37 CET
Support for finding fastest traces for deadlock properties has now been implemented (as of revision