How is the value of delays in transition determined in Concrete Simulator?

[denizcaygoz]

Hi,

When I simulate the models in concrete simulator. I see a value of delays in transition, in which the state isn't marked as commited.
The value of delays are different each time. As you can see I schreenshot.
I would like to know how the value of delays are determined? Are these complete random? Is there any interval of these delay values? or are they still within the scope of the transition constraints?

Delay Values

Models

[mikucionisaau]

Yes, the delay should be strictly within the scope of the model constraints.

In your highlighted steps two things happen: SmartHeatingSystem takes a transition after 1.02179 t.u. (I hope the temperature>=22 is true in that state, I cannot see), then after 18.9782 tempController takes the transition from Idle. If you sum up those two delays you get 20, which satisfies temp_timer == 20 constraint.

There is one caveat that some transitions might be missing in complex models with guards over dynamical variables (using ODEs): the transition list is populated based on pre-computatation into the future with respect to the given future horizon so transition with a guard beyond horizon might not be detected and hence omitted. For this purpose we provide "Expand" button to double the future horizon.
The longer horizons have additional computational cost (again, when using ODEs), thus there is also "Shrink" button to half the horizon.
The simple models (without ODEs) should not suffer from that.

Then the concrete simulator choices depend on this button (right-click on it to see the popup menu):

• Random means to pick uniformly from the transition list above (as if one was pointing and executing transitions blindly). This is useful to validate the model with respect to uniform feature coverage.

• Stochastic means to choose according to the probability distributions defined by the model, i.e. just like verifier would do: respect the uniform/exponential delays, probability weights on branching edges etc..

You may also want to inspect the trajectory of your variable values over time by right-clicking on the variable and choose Create new trajectory plot:

[denizcaygoz]

As I understood correctly that means all transition delays in SmartHeatingSystem should always be less than 20 right?.
Actually 20 was something I defined for tempController. How does this number also defines the interval for the delay time of tempController transitions?

There is also another problem I encountered:
I want to be able to verify time intervals between events/state changes.
For instance how can I define a Query for this system something like:
When event X occurs, the system reacts in X time units or
If X occurs, Z also occurs within Y time units.

I would like to say for instance:
When SmartHeatingSystem is in the state On and when the Guard condition is true then within X time units system will always end up in Off state.

How can I formulate this in Query?

Right now my query looks like this:
A<>(temperature >= 22 && temp_change_count < 2 && SmartHeatingSystem.On imply SmartHeatingSystem.Off)
But as you can see the part of "within Y time units occurs Z" is missing.

Here is my current system, if you need it. I made some changes, namely I replaced 20 with TEMP_UPDATE_INTERVAL = 60;
and replaced temp_values[15] with temp_values[15]

The main Specification of my system is that within Heating system will change to On and Off maximal 2 times within TEMP_CHANGE_COUNT_INTERVAL time unit.
As I say I also want to add a specifications like: within a certain time units if conditions are true, the system is able to switch the state On to Off or On to Off within X time unit

[mikucionisaau]

As I understood correctly that means all transition delays in SmartHeatingSystem should always be less than 20 right?.

Not necessarily. I do not see the dependencies in your model, so I can't say definately.

Actually 20 was something I defined for tempController. How does this number also defines the interval for the delay time of tempController transitions?

tempController has an invariant temp_timer<=20, so the delay from temp_timer==0 to temp_timer==20 in your trace was interrupted by SmartHeatingSystem transition and thus the 20 unit delay got split into two subsequent delays you have highlighted.

Note that invariants act globally: if one process has an invariant, then you may observe that other process dependent on the time flow, might get stuck or stutter until the first process leaves the location with invariant.

Please consult with Tutorial on UPPAAL on the semantics of timed automata.

There is also another problem I encountered:
I want to be able to verify time intervals between events/state changes.
For instance how can I define a Query for this system something like:
When event X occurs, the system reacts in X time units or
If X occurs, Z also occurs within Y time units.

This can be solved using leads-to property, see:
https://docs.uppaal.org/language-reference/query-semantics/symb_queries/#leads-to

Since you care about timing, then add a dedicated clock say clk, reset clk:=0 when X occurs and then your query can be written like this:

X --> Z and clk <= Y