I have written several requirements formally for modeling a real-time system. One of these requirements is as follows:
If sensor1.value is less than or equal to -5 and sensor2.value is less than or equal to 2, then eventually, after some time, sensor2.value will be greater than 2.
The formal representation of these requirements in LTL or TCTL is as follows:
Globally ((sensor2.value <= 2 and sensor1.value <= -5) -> EVENTUALLY sensor2.value > 2).
Based on this and other requirements, I have designed the following automaton(x is time variable).
My first question is whether I should consider the values of sensors as channels in the synchronization section of the automaton or as data variables in the guard section?
Now I want to see if my requirements are satisfied by timed automata or not. The automaton itself has no syntax errors. However, in the verifier section, I don't know how to write the queries.
Query for the case where sensor values are considered as data variables in the automaton:
A[]((automaton1.sensor1 <= 5) imply E<>(automaton1.sensor2 > 2))
When executing this formula, I encountered the following error.
Unexpected T_EF
In the second case, I also don't know how to design the query."
I just have some LTL formulas, and a Timed Automata(TA). (It's closer to mathematical definition of TA. no need to channel concept) I need to verify if TA satisfies formulas or not?