UPPAAL - 同步强制转换不起作用

Question

完全卡在上面了。 基本上，我有加热器、温度传感器和模拟温度升高的过程。 当温度高于某个值时，我希望加热器过渡到“禁用”状态。它可以与转换到异常温度状态同步。 但在模拟中，我只能在条件成立时获得可能性进行转换。 加热器： 温升管： 传感器：

我尝试为它添加同步： 传感器： 加热器： 但由于它无法在自动模式下改变状态，同步也不起作用...... 我怎样才能做到？

Answer 1

针对此案例的快速修复：

将

disable_heater

声明为

urgent

并且不允许延迟选项。

总的来说，这个解决方案不是一个好的设计。问题在于您的模型通过变量使用异步通信，这会引入更多状态并使其难以验证。更好的选择是使用同步通信。您已经可以使用

disable_heater

，但您还需要通过通道与临时立管同步，例如

temp_update!

。您将需要同步多个进程，以便您可以通过紧急或提交位置链接它们，或者使用

broadcast

通道（一个发送者多个接收者）。

请参阅 Uppaal 教程中关于价值沟通的部分。