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

3.1 The Design of the Customer
We consider the machine's interface, operated by the customer, as the simulation of
the customer's behavior. To make the system simple and general at first, the interface
is divided into two parts: the buttons and the slot. The names of different items label
the corresponding item buttons, and after the customer presses one of them, other item
buttons will be disabled, so that he can only choose one item in an order. Then the
customer can choose the “confirm” button to continue the order, where the slot will
indicate to him to put the coins in and the complete order will be sent to the vending
machine. If the customer chooses the “cancel” button, all the item buttons will be
enabled and he can start another order.
The vending machine will check the price of this order and whether the ordered
item is still available in its storage. If so, it will ask the slot to make the change. Then
the vending machine will deliver the product to the slot and enable the item buttons, if
the change can be made. Otherwise, the order will be refused and the payment is re-
turned to the customer.
3.1.1 The Interface Controller
According to the above requirement, the customer places his order of an item through
the buttons (including the item buttons and the command buttons: confirm and cancel)
on the machine's interface, so we design an interface controller to model these but-
tons, as well as the customer's interaction with the interface of the machine. A finite
set of actions for the item buttons and “confirm”, “cancel” buttons are specified in the
following design. The slot_get and slot_ret actions are designed to interact with
the slot component to obtain the payment from the customer. Meanwhile, we use the
order action to send the complete order to the vending machine, and after the order
has been processed by the vending machine, the order_ret action will be called to
reset the controller.
design component controller
in // the customer's payment in the slot
i_pay: int
prv b_item: array(int);
bt_g: bool; //guard for item buttons
bt_confirm: bool; //guard for confirm/cancel buttons
slot_g: bool; // guard for slot get action
s_req: bool;
ord_g: bool; // guard for order action
o_req: bool
out // order to vending machine
c_item: list (int);
c_pay: int
init ord_g = false ∧ o_req = false ∧ bt_g = true ∧ bt_confirm
= false ∧ slot_g = false ∧ s_req = false ∧ c_item = NULL
actions
button_select(id: int)[bt_g,c_item,bt_confirm]: bt_g,
false ->
bt_g' = false ∧ c_item' = c_item * b_item [id] ∧
bt_confirm' = true