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

design component slot
in // input coins from customer
i_cent: int;
i_nickle: int;
i_dime: int;
i_quarter: int;
i_dollar: int;
// received change amount and items from vending machine
r_change : int;
r_item: list(ITEM)
prv // coins storage
s_nickle: int;
s_dime: int;
s_quarter: int;
s_dollar: int;
// guards for action sequence
get_g: bool;
change_g:bool;
item_g: bool
out // changes made by the slot
o_nickle: int;
o_dime: int;
o_quarter: int;
o_dollar: int;
s_item: list (ITEM); // items to slot
o_pay: int; // payment amount to the controller
change_res: bool
init get_g = true ∧ change_g = true ∧ change_res = false ∧
item_g = false
actions
get_pay[get_g, s_nickle, s_dime, s_quarter, s_dollar]:
get_g ∧ i_cent = 0, false ->
get_g' = false ∧ s_nickle' = s_nickle + i_nickle ∧
s_dime' = s_dime + i_dime ∧ s_quarter' = s_quarter +
i_quarter ∧ s_dollar' = s_dollar + i_dollar
[] send_pay[get_g, o_pay]: ¬ get_g, false ->
get_g' = true ∧ o_pay' = 100*i_dollar + 25*i_quarter +
10*i_dime + 5*i_nickle
[] comp_change[change_g, change_res]: change_g, false ->
get_changed ∧ change_g' = false
[] send_change[change_g]: ¬ change_g, false ->
change_g ' = true ∧ (change_res = true ⇒ item_g ' = true ∧
s_nickle ' = s_nickle - o_nickle ∧ s_dime ' = s_dime -
o_dime ∧ s_quarter ' = s_quarter - o_quarter ∧ s_dollar ' =
s_dollar - o_dollar)
[] rec_item[s_item, item_g]: item_g, false ->
s_item' = r_item ∧ item_g' = false
[] rec_return[ret_g, s_item,]: true, false ->
s_item' = NULL ∧ get_changed
endofdesign