formal-verification - Uppaal - 当条件变为真时如何强制转换？

Question

我希望能够在条件变为真后立即强制转换。

例如，在此示例中，我想在全局变量a变为5时强制从下一个系统从状态S0转换到S1。守卫是不够的，因为在触发转换之前 a 达到 5 后仍然可以递增。我真的需要触发过渡，然后继续增加a。

有没有简单的方法来做到这一点？我尝试在状态中添加不变量，但它会造成死锁。

Answer 1

使用频道同步。几种方法：

1. 在进程上声明chan message;并添加message!同步increment，添加进程转换，并使用另一个带有保护的转换来检查值并相应地移动到另一个位置。message?nexta

2. 在边缘声明urgent broadcast chan ASAP;和使用，这将使该转换一旦启用（即满足防护）就变得紧急。紧急转换仅支持整数守卫。ASAP!next

Answer 2

您可以简单地a<=5在 S0 状态中添加不变量。