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

[] button_confirm[bt_confirm,slot_g]: bt_confirm, false ->
bt_confirm' = false ∧ slot_g' = true
[] button_cancel[bt_confirm,bt_g,c_item]: bt_confirm, false
-> bt_g' = true ∧ bt_confirm' = false ∧ c_item' = NULL
[] slot_get[slot_g,s_req]: slot_g, false ->
slot_g' = false ∧ s_req' = true
[] slot_ret[c_pay, s_req, ord_g]: s_req, false ->
c_pay' = i_pay ∧ s_req' = false ∧ ord_g' = true
[] order[o_req,ord_g]: ¬ o_req ∧ ord_g, false ->
o_req' = true ∧ ord_g' = false
// enable all the item buttons
[] order_ret[o_req, bt_g, c_item]: o_req, false ->
o_req' = false ∧ bt_g' = true ∧ c_item' = NULL
endofdesign
The input channel i_pay indicates the payment received from the customer. A fi-
nite set of item button actions (button_select) are defined, which correspond to the
sequence of item buttons on the machine's interface. These actions are examples of
schema actions indexed by the id (in the above sequence) of the item buttons. Such
schema actions may be used to describe succinctly a finite set of related actions, dis-
tinguishable by means of some index set. See [27] for a full explanation of such fami-
lies of actions and their precise semantics. We use a fixed size array b_item to store
the item's index in the storage of the vending machine, and the index of array b_item
will correspond to the id of the item button, e.g., the second item button b_item[2]
may correspond to the item index 6 in the item list of the vending machine's storage.
The workflow of the controller component is described as follows. After one item
button is selected, the guard bt_g is set to false to disable all the item buttons, so that
the customer can only choose buttons confirm or cancel (as the enabling guards of
other actions are disabled). If he chooses the confirm button, the guard slot_g is en-
abled and the slot_get action will be executed to request the customer's payment in
the slot component. If the cancel option is selected, the controller will enable all the
item buttons and wait for the customer's input of a new transaction. After the payment
is obtained from the slot, the order action will be called and it will send the order
Fig. 3. Graphical representation of the controller component