UPPAAL - Query Regarding Channel Related Property

Question

I am trying to make properties in which channels are used for example if X Channel signal is transmitted then this implies that Y Channel should send signal in response but I am facing an issue while making it. It generate an error so might be I am using the wrong template kindly guide me what is the exact syntax that should be used. I have tried it with 3 different ways but all fail and it gives " Server Exception: Type Error". Below is the syntax that I am using with THS and SP representing channels and THComponent and Cpacing are representing my templates/model.

1- A[ ] THS! implies SP!

2- A[ ] THComponent.THS implies Cpacing.SP

3- A[ ] THS implies SP

Can you kindly guide me what is the exact syntax?

Thanks

Answer 1

After A[] Uppaal expects a state property, but here it gets a channel/event instead -- this is not supported, you will have to reformulate the queries in terms of automata locations instead of channels.

Also, the implies from the second query is a simple implication, i.e. the whole expression is a state expression thus does not make sense in terms of events because event entail the change of state. You probably want a leads-to property, like:

p --> q

which is a shorthand for A[] p implies (A<> q) (note that the nested queries are not supported, thus this shorthand is very special).