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

In the above design, we assume the function to compute the composition of
change, namely get_change, has already been defined, which takes r_change as input
and computes the number of nickels, dimes, quarters and dollars. If the computation is
successful, it will set change_res to be true and the output channels for the change.
Otherwise, change_res is set to false and this event is sent to the vending machine.
Actually, get_change solves a linear programming problem, which takes s_nickel,
s_dime, s_quarter, s_dollar and r_change as parameters. To simplify the specification
of the slot component, we do not describe the detailed procedure here.
The workflow of the slot component is described as below. When the interface
controller requests the payment from the customer, the get_pay and send_pay actions
will be executed to provide the payment amount to the controller. After the vending
machine receives the order and recognizes that the payment is enough, it will ask the
slot to compute the change. So, the comp_change action is called and the result of
computation (change_res) is sent to the vending machine by the send_change action.
If the result is successful, the change is given to the customer by the slot and the
vending machine will send the product to the slot by means of the rec_item action.
Otherwise, the rec_return action will get the amount of payment from the vending
machine and give it back to the customer by calling the get_change function. The
graphical notation for the slot component is as follows, where we again suppress the
private channels and actions.
Fig. 4. Graphical representation of the slot component
3.2 The Design of the Vending Machine
Based on the functional requirement of the vending machine, we will divide it into
two components: vender and inventory, where the vender is in charge of the interac-
tion with the customer interface (controller and slot), and the inventory serves as a