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.
Created attachment 68 [details]
Test case system
This is the system that produces the error when generating the fastest trace.
Created attachment 69 [details]
Test case query
Query used to cause the error.
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.
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.
Support for finding fastest traces for deadlock properties has now been implemented (as of revision