memory - 无法验证 UPPAAL 属性

Question

我正在验证一个非常小的模型。但我收到内存耗尽消息。我多次更改模型但遇到同样的问题。我认为这个问题是由于使用用户定义的函数或使用选择选项来获取随机数。然后我改变了模型，没有调用函数，也没有使用选择选项，但仍然......我想知道这是 UPPAAL 的问题还是在我的模型中。除了内存耗尽之外没有错误。一旦在该 ctl 属性不起作用后更改了“r1”和“r2”的值。 CTL 适用于增量之前的所有 r1 和 r2 值。

Answer 1

该模型增加了几个变量（r1、r2 和 cntr）：如果它们没有上限（似乎没有，但我看不到所有函数），那么状态空间将会很大（所有值乘以位置数量，时间时钟区域），从而耗尽所有内存。

要么使这些变量有界（不允许增量传递某些值），要么将它们声明为元（如果您不了解后果，请不要这样做）。