Uppaal - How to force a transition when a condition becomes true?

Question

I would like to be able to force a transition as soon as a condition becomes true.

For example in this Example, I would like to force the transition from the system next from the state S0 to S1 as soon as the global variable a becomes 5. The guard is not enough because a can still be incremented once it reach 5 before the transition is fired. I really need the transition to be triggered and then continue to increment a.

Is there a simple way to do it? I tried by adding invariant in the state but it is creating deadlocks.

Answer 1

Use channel synchronization. Several approaches:

1. declare chan message; and add message! synchronization on the increment process, add message? on the next process transition, and use another transition with the guard to check the value of a and move to another location accordingly.

2. declare urgent broadcast chan ASAP; and use ASAP! on the next edge, this will make this transition urgent as soon it becomes enabled (i.e. the guard is satisfied). Only the integer guards are supported on urgent transitions.

Answer 2

You can simply add invariant a<=5 in the S0 state.