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

number of this item requested in the order. If so, it will call action inv_ret to return
inv_price > 0 (the total price of the items in ck_item); otherwise, it will return
inv_price = 0 in the inv_ret action. After the vender verifies that the change can be
made, it will call the req_item action, which is synchronized with the rec_req action
of the inventory, to get the ordered items and update the storage, and the inventory
has the send_item action to send the ordered items back to the vender.
Notice that in the count_item action we use the guard p_item != NULL to iterate
through the list of ordered items. It can be generalized as a mechanism to implement
the loop structures in the DynaComm language. (See future work.)
3.2.3 The Vending Machine Subsystem
According to our design of the vender and inventory components and the discussion
of their interactions, we can put them together by interconnecting the vender and the
inventory through a cable. The CommUnity Workbench like notation of Figure 5
describes the configuration diagram of the vending machine subsystem. The solid
circles attached to a component description represent elements of the interface of that
component. A line connecting two such interface elements, say sync1 of cable and
chaeck_inv of Vender, indicate that in the categorical diagram corresponding to that
of Figure 5, the regulative superposition from cable to Vender maps the action sunc1
to the action check_inv. So, this configuration diagram corresponds exactly to a well
defined and well formed diagram in the category of CommUnity designs and regula-
tive superposition morphisms. The colimit of this categorical diagram is the intended
semantics of the configuration.
The specification of the vending machine subsystem can be obtained easily from
the above configuration diagram and we do not describe it in detail here. We can also
determine the interface of this subsystem by looking at the left part interface of the
vender component in the diagram, which will interact with the interface controller and
the slot.
Fig. 6. Configuration diagram of the vending machine subsystem