model-checking - Uppaal - 通道同步 - 在评估警卫之前更新值

Question

我想做以下事情：

最初，我的变量x设置为 0，并且由于防护，此转换不可能触发。我希望能够将 x 的值更新为 1，然后检查b的转换保护以进行同步。我了解 Uppaal 首先进行转换（因此首先检查警卫），然后进行发送者的更新，然后是接收者的更新。

我发现解决此问题的唯一解决方案是使用已提交状态，如下所示：

我首先更新x然后进行同步。

它工作正常，但我想知道它是否存在更好的解决方案而不使用提交状态？