问题描述
例如，如果要传输X通道信号，那么我试图在其中使用通道的属性，这意味着Y通道应该发送信号作为响应，但是在制作时我面临一个问题。它生成一个错误，所以可能是我使用的模板错误，请指导我使用的确切语法是什么。我用3种不同的方法尝试了一下，但是都失败了，它给出了“ 服务器异常：键入错误”。下面是我使用THS和SP表示通道，THComponent和Cpacing表示我的模板/模型的语法。
1- A [] THS！暗示SP！
2- A [] THComponent.THS表示Cpacing.SP
3- A [] THS表示SP
请问我的确切语法是什么？
谢谢
解决方法
在A[]之后，Uppaal需要一个state属性，但是在这里它获得了一个通道/事件-不支持此操作，您将不得不根据自动机位置而不是通道来重新构造查询。
另外，第二个查询中的implies是一个简单的含义，即整个表达式是一个状态表达式，因此在事件方面没有意义，因为事件需要状态改变。
您可能需要一个潜在客户属性，例如：
p --> q
这是A[] p implies (A<> q)的简写
（请注意，不支持嵌套查询，因此此速记非常特殊）。