When I verify the query A[] not deadlock on my system without requesting a
diagnostic trace it works perfect and within few seconds I have the result
'property is not satisfied'. But when I do request a diagnostic trace, the
server crashes without giving any clue to the problem.

This problem came up after just a small change in my model. Before that change
checking of the query takes a very long time, I even haven't await the
termination of the verification. The latter was the case independently of
whether I requested a diagnostic trace or not.

I have found the cause of the crash: The small change consisted of changing an
invariant of a state and the guard of a self-loop of that same state.

Before the change the invariant was c<=r where c is a local clock in the
process and r is a global integer variable that represents a rate in beats per
minute. The guard on the self loop was c>=r.

Obviously this was wrong, because comparing a clock with a rate makes no sense.
So I changed the invariant and the guard into respectively c<=minute_length/r
and c>=minute_length/r

This change caused the crash when I checked the query A[] not deadlock with
requesting a diagnostic trace. Now I have created a function to convert a rate
to its corresponding time interval and the problem is gone.

Do you have any clue why Uppaal gets in trouble when using the mentioned
invariant and guard? Is it illegal to use such constructs in a model?


(In reply to comment #0)
> When I verify the query A[] not deadlock on my system without requesting a
> diagnostic trace it works perfect and within few seconds I have the result
> 'property is not satisfied'. But when I do request a diagnostic trace, the
> server crashes without giving any clue to the problem.
> This problem came up after just a small change in my model. Before that change
> checking of the query takes a very long time, I even haven't await the
> termination of the verification. The latter was the case independently of
> whether I requested a diagnostic trace or not.

Fixed in revision 3954.
The bug is missleading in fact. The problem comes from a bad computation
of ranges with divisions. The segfault comes from a lack of check on
trace generation, this was fixed previously.