Design in CommUnity with Extension Morphisms - Formal Methods and Hybrid Real-Time Systems - page 461

Fig. 7. Configuration diagram of the vending machine system

is true. They will not be disabled until the customer selects the confirm button, and
after the vending machine subsystem informs the controller that the order has been
processed by calling the order_ret action, all the item buttons will be reset.
We need to show that there exists an extension morphism from the old controller
component (say P 1 ) to controller' (say P 2 ). The morphism σ is defined as follows: the

mapping of the channels σ α will map each channels of P 1 to the identical channel of

P 2 , and σ γ defines the mapping of actions from each action in P 2 , to the identical ac-

tion in P 1 .

Lemma 1. σ is an extension morphism from P 1 to P 2 .

Proof
First we will show that

is a signature morphism. Since the mappings of channels
and actions are the identity, it is easy to see that all the conditions of a signature mor-
phism are satisfied, except possibly for the condition

σ

D 2 (g). Since the
actions in P 2 keep the effect of assignment to the mapped channels of P 1 , this condi-
tion also holds. Therefore,

σ α (D 1 ( σ γ (g)) ⊆

σ is a signature morphism.