uppaal - UPPAAL：作为函数参数给出的时钟是否具有方法或属性？

Question

我目前正在使用 UPPAAL v.4.1.19 并在帮助中看到可以将时钟作为函数参数给出。但是我找不到有关哪些方法或属性的任何信息，例如。时钟的下限和上限，可用于时钟。

示例函数：

void access_clock(clock & cl){
    //access clock here
}

是否有可能获得时钟的下限或在函数中用它做其他事情？

Answer 1

简短的回答：没有。

定时自动机模型只允许时钟比较（在守卫中）和分配（在更新中）。带有时钟参数的函数只能分配时钟变量。下限和上限是模型检查（符号分析）的结果，在模型之外，因此不属于模型本身。

据说时钟变量具有随时间增加的正实值——仅此而已，并且有意限制这种表达性，以便分析仍然可以确定。