我想了解更多关于定时自动机来验证实时系统的信息。目前，我正在尝试熟悉一个名为 UPPAAL 的工具。
我画了一些简单的图表并添加了不同的属性。整个模型应该代表一个生产单元系统，其中不同的机械单元相互传递一个块。
我已经模拟了块（BlockCycle）、2 个机械单元（Feeder、FeederBelt）和 2 个感应块到达的传感器。
尽管我认为我的系统会有意义，但它还是陷入了僵局：
这个转换的目标状态违反了不变量。这不是问题，只要您希望您的模型表现得像这样。
（不，我没有。;P）
不过，我似乎无法找到导致僵局的原因。该工具将我指向BlockCycle模型，但我没有在那里指定任何不变量。事实上，所有的转换要求都已满足，因此绝对应该进行转换（从Pos7到Pos8 ）。
下面您将看到系统如何演变并最终陷入困境（弹出错误消息）。
标签：
- 绿色：属性检查（例如FB_Running表示FB_Running == true）
- 深蓝色：属性更新/分配
- 深红色：位置（例如Pos7或Pos8）
具有相关转换的BlockCycle模型：
我的问题：为什么系统会死锁，即使仍然有可以采取的交易。
Edit1：当我删除 Sensor7 的位置Active（称为BlockAtPos[7]）的不变属性时，死锁就解决了。所以我猜，由于Sensor7和BlockCycle在死锁之前的最后一个转换之间没有同步，这会导致矛盾（BlockAtPos[7]在传感器还没有机会进行InActive转换时变为假），因此违反不变量。
注意：您可以在此处找到我的 UPPAAL 代码/文件：pcs.xml。