how can I model multiple synchronizations in UPPAAL? For example: The state change triggers two other state changes at the same time in different templates. In the synchronization field, I can only put one channel (sync1! or sync!). How can I combine sync1! and sync2! ?
Thanks
The easiest way to do this is to split the edge representing the state change into two and introduce a committed location in the middle. The first edge, leading from the source location to the committed location, should contain everything from the original edge except the second synchronization. The second edge, leading from the committed location to the destination location should contain the second synchronization.
Committed locations are virtual locations introduced to help modelling this kind of behavior. When an automaton enters a committed location it must leave it immediately without any time passing and it can only be interleaved with other automaton that are in a committed location. This also implies that a committed location will not be entered unless it can be left according to the rules.