【发布时间】：2021-03-22 16:32:26
【问题描述】：
我希望能够在条件变为真后立即强制转换。
例如在这个Example 中，我想在全局变量 后立即从状态S0 到S1 >a 变成 5。守卫是不够的，因为在触发转换之前 a 达到 5 后仍然可以递增。我真的需要触发过渡，然后继续递增a。
有简单的方法吗？我尝试在状态中添加不变量，但它会造成死锁。
【问题讨论】：
标签： formal-verification model-checking uppaal
【发布时间】：2021-03-22 16:32:26
【问题描述】：
使用频道同步。几种方法：
-
声明
chan message;并在increment进程上添加message!同步，在next进程转换上添加message?，并使用另一个带有保护的转换来检查a的值并移动到相应的另一个位置。 -
声明
urgent broadcast chan ASAP;并在next边上使用ASAP!，这将使此转换在启用后立即变得紧急（即满足防护）。紧急转换仅支持整数守卫。
【讨论】：
您可以在 S0 状态下简单地在a<=5 中添加不变量。
【讨论】：
-
您的答案可以通过额外的支持信息得到改进。请edit 添加更多详细信息，例如引用或文档，以便其他人可以确认您的答案是正确的。你可以找到更多关于如何写好答案的信息in the help center。
-
因此，当我们向状态添加不变量时，它是强制更新，但当我们向转换添加保护时，它不是强制更新，对吧？