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

database for storing the actual products (items) and maintaining the price and amount
of each item.
3.2.1 The Vender
The job of the vender is to accept the order from the customer (the accept action), ask
the inventory to check the price and amount of the ordered item(s) (actions check_inv
and check_ret), send the amount of change to the slot and ask if the change can be
made (actions change and change_ret), request the item(s) from the inventory (actions
req_item and req_return), deliver the item(s) to the customer (the delivery action) or
return the payment (the return_ord action), and inform the interface controller to be
reset to start a new order (the reset_controller action). The design of the vender com-
ponent is as follows, the meaning of the channels being explained in the comments.
design component vender
in // the ordered item(s) and payment from the controller
in_item: list(int);
in_pay: int;
// the price of the ordered item(s) from the inventory
inv_price: int;
inv_item: list(ITEM);
// the result of checking whether the change can be made
from the slot
chg_res: bool
prv // the set of guards to control the sequence of actions
ac: bool;
ck: bool;
cg: bool;
rt: bool;
rq:bool;
rc: bool;
dl:bool;
// stores the requested item(s) from the inventory
v_item: list(ITEM);
// stores the order and payment from the customer
ord_item: list(int);
ord_pay: int
out // the order and payment to be sent to the inventory
ck_item: list(int);
ck_pay: int;
// the amount of change to be sent to the slot
chg_amt: int;
// the ordered item(s) sent to the customer
out_item: list(ITEM);
// the returned amount of payment to be sent to the slot
ret_amt: int
init ac' = false ∧ ck' = false ∧ cg' = false ∧ rt' = false ∧
dl' = false ∧ rq' = false ∧ rc' =false
actions
[ac, ord_item, ord_pay, ck]: ¬ ac, false ->
ac ' = true ∧ ord_item ' = in_item ∧ ord_pay ' = in_pay ∧ ck '
= true