提问人：Yarik.Yar 提问时间：11/1/2023 更新时间：11/4/2023 访问量：22
UPPAAL - 使用同步器进行强制转换不起作用
UPPAAL - force transition with synchro doesn't work
问：
完全卡在上面。
基本上，我有加热器、温度传感器和模拟温度升高的过程。
我希望加热器在温度高于某个值时过渡到“禁用”状态。它可以与过渡到异常温度状态同步。
但在模拟中，我只有在条件为真时才有可能进行转换。
加热器： 温度提升器： 传感器： 
我试图像这样为它添加同步：
传感器： 加热器： 
但是由于它不能在自动模式下改变状态，同步器也不起作用......
我怎样才能做到？
答：
0赞
mariusm
11/4/2023
#1
特定于此案例的快速修复：
声明 as 和 will not allow delay 选项。disable_heaterurgent
一般来说，这个解决方案不是一个好的设计。问题在于，您的模型通过变量使用异步通信，这引入了更多状态，并且难以验证。更好的选择是使用同步通信。您已经在使用 ，但您还需要通过通道与临时转接卡同步，例如 。您将需要同步多个进程，以便通过紧急或承诺位置链接它们，或者使用通道（一个发送方多个接收方）。disable_heatertemp_update!broadcast
请参阅Uppaal教程中关于价值沟通的部分。
评论