Concluding the Example
The developed model has no undesired states. It conforms with the initial animation description.
There are no deadlocks, since the control statements will always put the animation in a valid state.
There are two mutually excludent transitions, confirming the behavioral restriction.
The only mutually dependent transitions, with di,j = 1, are associated to events of the same object, either sphere A or sphere B.