Information Technology Reference
In-Depth Information
prv
// stores the ordered item(s)
p_item: list (int);
r_item: list (int);
p_price: int;
// array index is item id
db: array (ITEM, int, int);
// stores the amount of each ordered item, all the en-
tries are initialized to be 0.
s_item: array (int);
j :int;
// the guards to control the sequence of actions
price_g: bool;
amt_g: bool;
ret_g: bool;
send_g : bool
out
o_item: list (ITEM);
// the price of the order sent to the vender
o_price: int
init
p_item = NULL
∧
price_g = false
∧
amt_g = false
∧
ret_g
= false
∧
o_price = 0
∧
o_item = NULL
∧
r_item = NULL
∧
send_g = false
actions
check[]: true, false -> p_item' = i_item
[]
prv
count_item[]: p_item != NULL, false ->
s_item[head(p_item)]' = s_item[head(p_item)] + 1
∧
p_price' = p_price + second(db[head(p_item)])
∧
p_item' =
tail(p_item)
∧
(tail(p_item) = NULL
⇒
price_g' = true)
[]
prv
check_price[: price_g, false ->
price_g
'
= false
∧
((i_pay >= p_price
⇒
amt_g
'
= true
∧
j
'
= 1)
∨
(i_pay < p_price
⇒
ret_g
'
= true
∧
o_price
'
= 0))
[]
prv
check_amt[]: amt_g
∧
(j <= sizeof(db)) , false ->
((s_item[j] <= third(db[j])
⇒
j
'
= j + 1
∧
(j =sizeof(db)
⇒
ret_g
'
= true
∧
o_price
'
= p_price))
∨
(s_item[j] >
third(db[j])
⇒
amt_g
'
= false
∧
o_price
'
= 0
∧
ret_g
'
=
true))
[] inv_ret[]: ret_g, false -> ret_g' = false
[] rec_req[]: true, false -> r_item' = i_item
[]
prv
get_item[]: r_item != NULL, false -> o_item ' =
o_item * first(db[head(r_item)])
∧
third(db[head(r_item)])' = third(db[head(r_item)])-1
∧
r_item' = tail(r_item)
∧
(tail(r_item) = NULL
⇒
send_g'
= true)
[] send_item[]: send_g, false -> send_g' = false
endofdesign
The workflow of this component is as follows. First, the check action is called to
enable the guard of the count_item action. Then the action check_price is called to
decide if the total price is less than ck_pay. If so, the inv_ret action will be enabled to
return the result (inv_price) to the vender. Otherwise, the check_amt action is exe-
cuted to check if the amount of each ordered item in the inventory is greater than the
Search WWH ::
Custom Search