无法验证UPPAAL属性

Question

我正在验证一个非常小的模型。但是我收到了内存耗尽的消息。我更改了模型几次，但都有同样的问题。我认为这个问题是由于使用用户定义的函数或使用select选项来获取随机数造成的。然后我更改了模型，没有调用函数，也没有使用选择选项，但仍然...我想知道这要么是UPPAAL的问题，要么是我的模型。除内存耗尽外，没有其他错误。一旦"r1“和"r2”的值在ctl属性不起作用后被更改。

CTL适用于递增前r1和r2的所有值。

Answer 1

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

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