Information Technology Reference
In-Depth Information
(c_item, c_pay) to the vending machine, then wait for the result of the order. After the
vending machine processes the order and indicates the result to the order_ret action of
the controller, the order_ret action will reset the item buttons and the c_item list, to be
ready to accept another order. The graphical notation for the (syntax of the) controller
component is shown in Figure 3 (we suppress private channels and actions):
Notice that we use a number of guards to control the sequence of actions in the
controller, and the correctness of our design can be ensured by maintaining the right
workflow of the component through the appropriate use of these guards. We also use
the list data structure to record the ordered items, although currently only one item is
allowed in the order. The reason is that in the different kinds of design morphisms we
have discussed so far, the mapping of channels requires the types of channels to be
preserved. (Refinement morphisms do not support data refinement, so a refinement
solution to get around this problem is not available.) If we use one channel of integer
type to record the ordered item now and there is a new requirement to allow the cus-
tomer to select multiple items in an order, we have to add new channels to the com-
ponent and modify the corresponding actions as well, which seems awkward. There-
fore, we choose the list data structure for the ordered items and the corresponding
actions are designed to process the list of items.
We have also designed a pattern for a pair of actions of one component (e.g.
slot_get and slot_ret), which sends a request to another component and waits for its
response to proceed. The trick is to assign a guard (initialized to be false) to the call-
back action to make sure that it will not be called arbitrarily in an unexpected situa-
tion, and it will only be enabled in the request action.
3.1.2 The Slot
The slot component takes care of the acceptance of the customer's payment and de-
cides if the correct change can be made depending on its current store of coins. When
the interface controller requests the payment from the customer, the slot will distin-
guish the various kinds of coins and it will refuse the payment and indicate this event
to the controller if there exists an illegal coin in the customer's input. Otherwise, it
will store the coins and send the payment amount to the controller. Regarding the
function for making the change, the slot is able to compute the composition of coins
for the amount of change requested by the vending machine, based on its current
store. If the computation is not successful, the vending machine will refuse the order
and inform the slot to return the payment, which can certainly be made.
In the following design of component slot, a set of input channels such as i_dollar,
i_quarter, etc. represents the payment from the customer, a set of private channels is
included as the coin store of the slot, and we also use output channels o_nickel,
o_dime, o_quarter and o_dollar to represent the change made by the slot. The get_pay
action stores the coins in the payment and the send_pay action puts the amount of
payment in the output channel o_pay. According to the amount of change that should
be made in the input channel r_change, the comp_change action will compute the
composition of coins, and the send_change action will send the result of the computa-
tion (change_res) and update the storage of coins if needed. While the ordered item is
accepted by the action rec_item, and the rec_return action receives the returned pay-
ment amount and returns the coins to the customer.
Search WWH ::




Custom Search