2.2.3 Transitions $T$

$T$ is a set that contains all the transitions in a model. A transition, when enabled, changes the model from the source state to the destination state. A transition is enabled if and only if the following conditions are all satisfied:

1. The model is in the source state $SRC$.

2. Event $E$ is received and is at the head of the global event list (a logical list that contains all the events to be processed by a model in the sequence of their arrival).

3. All the formal parameters defined in $\gamma$ have their values of the correct types (if the specific implementation supports types).

4. Guard $G$ is valid and evaluated to $true$.

Provided that the guard (though it is implementation-dependent) is only a boolean expression without any side effect (i.e., potential change to the model state), and the execution of a transition is in a critical section so that no other actions affect the decision, the order of the above conditions is not important. For example, if a specific implementation uses exactly the same order to decide enabled transitions, it may ignore the evaluation of guards if any one of the first three conditions is not satisfied. (This method is known as short-circuit.)

There may be more than one transition (in the same component) enabled by a single event. In that case, the transition with the highest priority is fired, which means its $\lambda$ is executed, and the state changes to $DES$.

$\gamma$ is a set of variables that act as formal parameters received with the event $E$. If a transition requires parameters, the event must provide at least the same number of parameters with the same types (if types are supported). It may even provide more parameters (after those required), which are simply omitted.

$\lambda$ is a list of sequentially executed output actions. Control structures such as loops and if-else conditions are not allowed. Those structures must be explicitly modeled (see section 5.5). $\lambda$ may contain actions that further broadcast events. If such actions are included, the newly broadcast events are appended to the end of the global event list.

$HS_T$ is used in combination with $HS$ of a state. However, $HS_T$ is ignored if the $HS$ property of the destination state $DES$ is $None$.

$Prio$ is an arbitrary integer that represents transition priority. The smaller this number is, the higher priority the transition has. However, this number is used only for conflicts that cannot be resolved by the scheme of transition ordering (see section 2.2.5).