Information Technology Reference
In-Depth Information
Fig. 5. Graphical representation of the vender component
Again, we use a set of guards to control the sequence of actions in the vender com-
ponent, and, in the above explanation of the component's work mechanism, we are
able to control the right workflow of the design through the appropriate use of these
guards, so that the correctness of our design can be ensured.
3.2.2 The Inventory
The inventory component maintains a list of items along with their price and remain-
ing amount: (item_id:int, item:ITEM, price:int, amount:int), where item_id is the
item's index in the storage and item represents the real item product. We use an array
db (with a fixed size) to store this list of items, and the index of this array corresponds
to item_id. Meanwhile, we assume functions first, second and third have been defined
to return the first, second and third member of db, respectively.
The private action count_item calculates the amount of each ordered item and
stores it in the channel s_item. It also computes the total price of the order. The
check_price action goes through the inventory database and compares the amount of
each ordered item with the amount of that item in the storage. If the storage is not
enough or the payment is less than the price of the order, the output channel will be
set to 0; otherwise, it will set to the value in p_price. The get_item action will retrieve
the items from the storage according to the order and update the db channel. The
specification of the inventory component is as follows:
design component inventory
in
// the ordered item(s) and payment from the vender
i_item: list (int);
i_pay: int
Search WWH ::




Custom Search