model-checking - 如何在 UPPAAL 中获取时钟的当前值并将其存储在整数变量中？

Question

谁能告诉我如何获取时钟变量的当前值并存储在一个整数变量中。我试过 k=t（其中 k 是整数，t 是时钟），但它会引发“不兼容的类型错误”。我也尝试过 k=(int)t，但它会引发“Unexpected T_INT”语法错误。

UPPAAL 中的时钟是否有任何类型转换可用于获取时钟的当前值并将其存储在变量中？

Answer 1

这是不可能的，因为时间的处理方式（象征性地）。如果您使用 UPPAAL 模拟器，您可以看到时钟值没有具体表示，而是作为时钟约束。因此，您不能真正谈论时钟是某个值，而是当前时钟估值满足许多约束，因此时钟处于某个区间。

您没有指定要实现的目标，因此有一些相关的指针：

• 但是，您可以将时钟与整数变量进行比较
• 如果您想知道时钟可以达到的最大值，可以使用“sup:clock”查询