Uppaal - 如何在条件成立时强制转换？

问题描述

我希望能够在条件成立时立即强制转换。

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

有简单的方法吗？我尝试在状态中添加不变量，但它会造成死锁。

解决方法

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

1. 声明 chan message; 并在 message! 进程上添加 increment 同步，在 message? 进程转换上添加 next，并使用另一个转换与守卫检查 a 的值并相应地移动到另一个位置。

2. 声明 urgent broadcast chan ASAP; 并在 ASAP! 边上使用 next，这将使此转换在启用后立即变得紧急（即守卫得到满足）。紧急转换仅支持整数保护。