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 1424).