0

我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]?_

那里可能出了什么问题？

4

1 回答 1

0

如果您的数组长度为 3，则索引需要为 0、1 或 2。这就是索引值 3 超出范围的原因。确保您的索引永远不会大于 arraylength-1。

于 2018-10-11T16:05:10.613 回答