0

我正在尝试创建使用通道的属性，例如，如果 X 通道信号被传输，那么这意味着 Y 通道应该发送信号作为响应，但是我在制作它时遇到了问题。它会产生一个错误，所以可能是我使用了错误的模板，请指导我应该使用的确切语法是什么。我尝试了 3 种不同的方法，但都失败了，它给出了“服务器异常：类型错误”。下面是我使用 THS 和 SP 表示通道的语法，THComponent 和 Cpacing 表示我的模板/模型。

1- A[ ] THS！暗示SP！

2- A[ ] THComponent.THS 暗示 Cpacing.SP

3- A[ ] THS 暗示 SP

你能指导我确切的语法是什么吗？

谢谢

4

1 回答 1

0

在A[] Uppaal 需要一个 state 属性之后，但在这里它获得了一个通道/事件——这不受支持，您将不得不根据自动机位置而不是通道来重新制定查询。

此外，implies 来自第二个查询是一个简单的暗示，即整个表达式是一个状态表达式，因此就事件而言没有意义，因为事件需要状态的改变。您可能需要一个潜在客户属性，例如：

p --> q

这是一个简写A[] p implies (A<> q) （注意不支持嵌套查询，因此这个简写非常特殊）。

于 2020-09-21T08:05:13.233 回答