|Summary:||Fastest trace error|
|Product:||UPPAAL||Reporter:||Mark Pavlidis <pavlidmh>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
|Version:||3.6 Alpha 1|
Test case system
Test case query
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 1424).