UPPAAL - force transition with synchro doesn't work

Question

Totally stuck on it. Basically, I have heater, temp sensor and process that simulates rise of temperature. I want heater to transite to "disabled" state when temp is above some value. It can be synchronised with transition to abnormal temp state. But in simulation I can only get possibility to make transition when condition is true. heater: temp riser: sensor:

I tried to add synchro for it like that: sensor: heater: But since it can't change state in automatic mode, the synchro also doesn't work... How can I make it?

Answer 1

A quick fix specific to this case:

Declare the disable_heater as urgent and will not allow delay option.

In general this solution is not a good design. The issue is that your model uses asynchronous communication through variables, which introduces many more states and makes it hard to verify. A better option is to use synchronous communication. You are already on your way by using the disable_heater, but you also need to synchronize with temp riser through channel, eg temp_update!. You will need to synchronize multiple processes so you either link them through urgent or committed location, or use broadcast channel (one sender multiple receivers).

Please see Uppaal Tutorial section on value communication.