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

Bug 222

Summary:	Fastest trace error
Product:	UPPAAL	Reporter:	Mark Pavlidis <pavlidmh>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	minor
Priority:	P2
Version:	3.6 Alpha 1
Hardware:	All
OS:	All
URL:	http://mark.pavlidis.org/code/uppaal/
Architecture:
Attachments:	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).