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

• L Ei (g) ⇒ n'(L θ (n' γ (g))).

U Ei (g) ⇒ n'(U θ (n' γ (g))).
From our definition of “middle” design, L θ (n' γ (g))

•

⇔ true, U θ (n' γ (g)) ⇔ true, so these

two conditions hold.
With this property, in a well-formed configuration diagram, we are able to replace
a component by its extension component, by combining the regulative superposition
from the cable to the old component with the extension morphism between the old
component and its extension, to obtain a new regulative superposition from the cable
to the extended component. If we build several extensions, each built on top of the
previous one, then the fact that extensions compose in the category of CommUnity
designs and extension morphisms guarantees that this composition is an extension.
Hence, the above result still applies when we build extensions incrementally. There-
fore, we reach the conclusion that in a well-formed configuration diagram of a
system, we can extend any subcomponents of the system (through extension mor-
phisms), and thus obtain an updated well-formed configuration diagram only con-
taining regulative superpositions, through which the semantics of the new system
can be derived from its colimit. Moreover, it can be shown that the colimit of the
new configuration diagram is an extension of the colimit of the old configuration
diagram [8].
By examining the proof of proposition 8, we can see that, if θ i is not a cable, the

composition of a regulative superposition and an extension morphism may not give a
regulative superposition. Therefore, it is necessary to enforce designs to be intercon-
nected by cables in a well-formed configuration diagram, so that the colimit will exist
after extending any of the designs in the diagram through extension morphisms. (This
result mimics the properties of refinements in the context of cables and regulative
superpositions.)

3 An Example Vending Machine System

Now we want to model a system consisting of a customer and a vending machine with
the DynaComm language, to illustrate the use of hierarchical design and then to illus-
trate the use of extension morphisms to enable us to modify our design in a way not
allowed by refinements and regulative superpositions. The requirement of this system
is described as follows: The vending machine maintains a list of items, along with the
price and amount of each item. The customer can place an order by inputting the
name of the item and the payment to the vending machine. Initially, we only allow the
customer to order one item in a transaction; this will be extended later. The vending
machine will check the price of the item and decide if the order is accepted. If so, it
will deliver the item along with the change to the customer; otherwise, the payment is
returned to the customer. Initially, the vending machine will only accept payment
comprised of nickels, dimes, quarters and loonies (Canadian single dollars using the
image of a local bird), so it will refuse the order if the customer puts a one cent piece
in the payment slot. Meanwhile, if the vending machine is not able to make the
change, it will also refuse the order and return the payment.