How to test, as a query, whether when Guards X is true the delay time between transitions from state A to state B is always less than a Y time interval.

[denizcaygoz]

I want to know if I can test with UPPAAL if the delay between transition state a to state b happens always less than given timed unit.

so in my example
I want to test from the time when Guard is true, the transition delay duration from Off to On always less than given timed unit.
Can I express this as Query and how can I measure/save that delay and express it as Query?

In concrete simulator I actually can see in how much time units delay system goes from Off to On but I want to test this in Query.

When an event X (condition X) happens, must the system go from state A to state B within Y time intervals.
I'm thinking this is something that I should be able to test/write as a query with a tool like UPPAAL.

[mikucionisaau]

1. declare a extra clock, say x
2. add a reset x:=0 to all edges leading to SmartHeatingSystem.Off
3. stop the clock x in SmartHeatingSystem.On with invariant x'==0
4. check the query: A[] SmartHeatingSystem.On imply x<=timeout

Steps 3 and 4 can be simplified if you want to check that SmartHeatingSystem does not stay in Off longer than timeout:

• A[] SmartHeatingSystem.Off imply x<=timeout.
• Compute the upper limit of x with query sup{SmartHeatingSystem.Off}: x

[denizcaygoz]

1. ✅
2. ✅
3. ❌ I can't define x'==0. And what's x'. Do you mean x?
   

Also I want to actually check "Starting From the time when the Guard (from Off to On) is true, with how much delay can transition from Off to On take place? Is this time always lower than the timeout?
I can see this amount of time as delay in Concrete simulator but I have to check as a Query.