Ошибка проверки UPPAAL - значение индекса находится вне диапазона

Question

Я использую Uppaal для проверки системы. Симуляция работает отлично, но когда я проверяю это свойство A[] not deadlock, оно выдает мне следующую ошибку:

_The successors of this state are not well defined.
Index value 3 is out of range. Array length = 3, Element size = 1 in line 1 of go3[id]?_

Что там могло пойти не так?

Answer 1

Если ваш массив имеет длину 3, индекс должен быть 0, 1 или 2. Вот почему значение индекса 3 выходит за пределы диапазона. Убедитесь, что ваш индекс никогда не превышает arraylength-1.