Search code examples
model-checking

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

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?

Solution

  • 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])