UPPAAL鞋厂并行系统建模遇死锁：满足条件却无法触发红转移

这种情况在UPPAAL建模并行系统时很常见——别光盯着p≥4这个Guard条件，还有很多隐藏约束会阻止转移触发，我给你列几个最可能的排查方向：

• 源位置的不变量（Invariant）限制
  先检查红色转移的源状态有没有设置不变量。比如如果源位置的不变量是p ≤ 20，那当p=21时，这个状态的不变量已经不满足了，你的自动机根本不可能停在这个源位置，自然触发不了从这里出发的转移。你可以双击源位置查看它的不变量表达式。

• 同步通道的匹配问题
  如果这个转移带有同步标签（比如some_chan!或者some_chan?），那转移触发的前提是存在对应的同步伙伴：比如你这边是发送操作，就得有另一个自动机处于能接收该同步信号的状态。如果没有匹配的伙伴，哪怕Guard满足，同步也做不成，转移就卡着触发不了。

• 变量作用域的坑
  确认p是全局变量还是当前自动机的局部变量？如果是局部变量，UPPAAL里每个并行实例都有自己的p副本——你看到的p=21可能是其他实例的数值，当前这个自动机实例的p其实没达到4。你可以在模拟器里选中这个自动机实例，查看它的局部变量值，别搞混了全局和局部。

• 转移优先级或抢占设置
  看看是不是给其他转移设置了更高的优先级？UPPAAL里优先级高的转移会优先执行，哪怕你的转移Guard满足，也会被高优先级的转移抢先。另外如果有抢占式转移（比如设置了urgent或者committed属性），也可能直接阻止当前转移的触发。

• 并行实例的全局资源冲突
  因为你有5个并行运行的系统，可能存在全局资源竞争：比如这个转移需要获取某个共享资源，但该资源被其他实例占用了，哪怕p≥4满足，拿不到资源也触发不了转移。可以检查模型里有没有全局的资源变量（比如mutex之类的），看看当前资源的占用状态。

调试小技巧 #

用UPPAAL的模拟器一步步执行，重点看：

1. 当前自动机实例是否真的处于转移的源位置？
2. 源位置的不变量是否和当前变量值兼容？
3. 转移的同步标签有没有对应的伙伴？
4. 当前实例的p值到底是多少（别被全局变量或其他实例的数值误导）？

内容的提问来源于stack exchange，提问作者Balazs F.