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

[] check_inv[ck, ck_item, ck_pay]: ck, false ->
ck_item ' = ord_item ∧ ck_pay' = ord_pay ∧ ck ' = false
[] check_ret[cg, rt, v_item]: true, false ->
(inv_price >= 0 ⇒ cg ' = true) ∨ (inv_price = 0 ⇒ rt ' =
true)
[] change[cg, chg_amt]: cg, false ->
chg_amt' = ord_pay inv_price ∧ cg ' = false
[] change_ret[rq, rt ]: true, false ->
(chg_res = true ⇒ rq ' = true) ∨ (chg_res = false ⇒ rt '
= true)
[] req_item[rq, ck_item]: rq, false ->
ck_item ' = ord_item ∧ rq ' = false
[] req_return[v_item, dl]:true, false ->
v_item ' = inv_item ∧ dl ' = true
[] return_ord[rt, ret_amt, out_item, ac, rc]: rt, false ->
rt ' = false ∧ ret_amt ' = ord_pay ∧ out_item ' = NULL ∧
rc ' = true
[] delivery[dl, ac, out_item]: dl, false ->
dl ' = false ∧ out_item ' = v_item ∧ rc ' = true
// inform the controller to accept another order
[] reset_controller[rc]: rc, false ->
rc ' = false ∧ ac ' = false
endofdesign
According to the initialization condition of this design, only the accept action is
enabled and it is synchronized with the order action of controller to accept the order
of the customer. It also sets the guard ck to be true, so that the check_inv action will
be executed to ask the inventory to check the price and amount of the ordered item(s).
The check_ret action waits for the response from the inventory: if inv_price>=0, it
means that the transaction can continue and this action sets the guard cg to be true, to
call the slot to check if the change can be made; otherwise, it enables the guard rt to
call the return_ord action, if any item is not available or the payment is not enough.
If the order can continue, the change action is synchronized with the comp_change
action of the slot to make the appropriate change to the customer. Then the change_ret
action will wait for the response from the slot indicated by the input channel chg_res:
if the change can be made, the vender will request the item from the inventory using
the req_item action, which is synchronized with the rec_req action of the inventory;
otherwise, the return_ord action is called to return the payment. After the vender re-
ceives the requested item from the inventory using the req_return action, the delivery
action will be called, which is synchronized with the rec_item action of the slot to
deliver the item. Otherwise, the action return_ord will be executed and the slot's ac-
tion rec_return will be synchronized to return the payment to the customer. Finally,
the vender will call the reset_controller action to synchronize with the order_ret
action of the controller to inform it that the next order can now be taken.
The graphical notation for the vender component is depicted in Figure 5 below (we
ignore private channels and actions).