无法验证 UPPAAL 属性

【问题标题】：Unable to verify UPPAAL properties无法验证 UPPAAL 属性
【发布时间】：2018-11-27 22:14:00
【问题描述】：

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

【问题讨论】：

标签： memory out-of-memory deadlock verification uppaal

【解决方案1】：

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

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

【讨论】：

r1 和 r2 用于在范围之间运行时钟。当时钟接近 r2 时，我将一些随机数分配给地址（使用函数 assign()）。 r1 和 r2 的值仅用于迭代目的。我不想保存过去的值。我如何向您展示完整的模型。请给我一些链接，我将分享详细模型。