calculate conditional cumulative duration in UPPAAL

[Szpilman2]

Dear UPPAAL Team,

I hope this message finds you well.

I have two timed automata named "Software" and "Hardware". I have attached pictures of the models.

Software:

Hardware:

Whenever the Software TA sends a signal through the "use" channel, the Hardware TA receives the signal and transitions to the "using" state. The Hardware remains in the "using" state for a short period (in my case, 2 units of time) before transitioning to the "tail" state.

I have got two questions:

1. Based on the provided automata (software/hardware), we know that for each "use" signal, the hardware transitions to the "Tail" state and remains there for a specific duration. I want to write a query to find the sum of the durations that the hardware remains in "Tail," provided each duration is greater than a specified constant, while ignoring durations that are less than this constant. I am unsure how to achieve this. Is there a way to do this in UPPAAL?

2. Is there a way to calculate the time spent in the "Tail" state for each "use" signal individually? In other words, I want to determine the duration the hardware remains in the Tail state for each "use" signal in the software TA. I am aware of a naive solution where, in the update of the outgoing edge of the "Tail" state, I set sw = 0 and, for each use, write the query bounds{software.goal_use_state}: sw. However, this approach requires writing numerous queries based on the number of use states. Is there a more wisely approach to achieve this?

Could you possibly help me with this?

also this is my model:
EnergyHotspotModel_withSojuorn.zip

Thank you for your assistance.

Best regards,
Peyman

[mikucionisaau]

As for the first question, your model already uses sw stop-watch, so the total sum is just supremum value:

sup: sw

If you want to differentiate delays by some constant, then you will have to split Tail location into several and model the stop-watch accordingly.

For the second question, the naive approach currently is the only way. UPPAAL used to have state space reuse option, which could help a bit with multiple queries, but this functionality needs to be recovered.

Alternatively, we need to implement a different bounds query which would accept multiple predicates and collect separate data for each.

[Szpilman2]

Dear Marius, Thank you very much for your help; I truly appreciate it.