Different body actions, though they may require different input, must produce output to the same set of output pins. So no matter which body action is executed, the output of the conditional action is always complete.
One might notice from the figure that a conditional action is not explicitly associated with input pins or output pins. It is only associated with available input pins and available output pins, since the input and output is implicitly given by or given to the execution context of the conditional actions.
As another underlying rule, there should be no data flow between two clauses of a conditional action.
Clauses can have noncyclic predecessor-successor relationships among them. In this way, a clause may be defined as a successor of some others, meaning that its test action (and body action if possible) is executed after the predecessors. Of course, according to the rule that exactly one clause gets executed at a time, if any of its predecessors is executed, the successor clause could not be executed. Test actions of unrelated clauses may be executed concurrently.
An application of the clause relationship is to define a default body action for the conditional action: the default action is specified as the successor of all other clauses and its test action always return true.
In this way, clauses form a hierarchy. Test cases in each level of the hierarchy must be mutually exclusive, though they may not cover all possible conditions.
The above assertion assures the model to be deterministic under all conditions. This conforms to the well-formedness rule in [AILKC+00].
