Deadlock check vs. out-of-range array lookup Uppaal

Question

When I run the A[] not deadlock query in the Verifier on my model, the verification stops with error:

The verification was aborted due to an error. Most likely, this is caused by an out-of-range assignment or out-of-range array lookup.

Does this mean implicitly that my model is deadlock-free until the "out-of-range assignment or out-of-range array lookup" happens?

Answer 1

The solution was extending the query with the index variable when checking for deadlock, like

A[] not deadlock || indexVarble => 24

So if there is a deadlock, it should be when we run out of range. (in the example the range was [0-23])

Answer 2

It would not make sense for UPPAAL to continue searching the state-space if it is able to answer to query. So I think you can assume that the part of the state-space UPPAAL managed to search is deadlock-free.

Just remember that it might be possible to reach the error state through multiple traces but that dependents on your model.

It sounds like you already know why you get this error. You could try to fix it by adding a guard !willCauseError() to the model that ensures that you never end up in this error-state. That in itself might cause a deadlock though. To avoid that you can add a transition from the relevant location to itself with the opposite guard willCauseError(). This will force the program into a livelock instead of a deadlock.