module COMMERCE_PROCESSES (COMMERCE_TYPES) is

channel ENQUIRY is
   (p: Product, q: Nat)
end channel

-------------------------------------------------------------------------------
-- Local store process for the stock management system
-------------------------------------------------------------------------------

-- A local store can send requests to the central store. If a request succeeds,
-- the local stock is updated.
-- The interaction of a local store with its clients is not modeled: the local
-- stock only increases.
 
process LocalStore [request: ENQUIRY, ok, nok: none] (in var s: Stock) is
   var p: PRODUCT in
      loop
         p := extract (s);
         request (p, 5 of Nat);
         alt
            ok;
            s := increase (p, 5, s)
         []
            nok
         end alt
      end loop
   end var
end process

-------------------------------------------------------------------------------
-- Central store process for the stock management system
-------------------------------------------------------------------------------

-- The central store can receive a request from a local store or emit a request
-- to a supplier. In case of reception of a request from a local store, the
-- answer (ok or nok) is computed depending on the availability of the product
-- in the stock. If items are delivered (in reponse to a request from a local
-- store) or received (in response to a successful request to a supplier), the
-- stock is updated accordingly.
 
process CentralStore [request_local: ENQUIRY, ok_local, nok_local: none,
                    request_supplier: ENQUIRY, ok_supplier, nok_supplier: none]
                    (in var s : Stock) is
   var p: PRODUCT, q: Nat in
      loop
         alt
            -- request received from a local store
            request_local (?p, ?q);
            if isAvailable (p, q, s) then
               -- quantity available
               ok_local;
               -- products delivered: update the stock
               s := decrease (p, q, s)
            else
               -- quantity not available
               nok_local
            end if
         []
            -- request sent to a supplier
            p := extract (s); -- choose the first product out of stock
            request_supplier (p, 5 of Nat);
            alt
               ok_supplier;
               -- successful request: update the stock
               s := increase (p, 5, s)
            []
               nok_supplier
            end alt
         end alt
      end loop
   end var
end process

-------------------------------------------------------------------------------
-- Supplier process for the stock management system
-------------------------------------------------------------------------------

-- A supplier can receive requests from the central store. If the stock
-- permits, the request is fulfilled, and the stock updated. 
-- The production of items by a supplier is not modeled: the stock of a
-- supplier only decreases.

process Supplier [request: ENQUIRY, ok, nok: none] (in var s: STOCK) is
   var p: PRODUCT, q: Nat in
      loop
         request (?p, ?q);
         if isAvailable (p, q, s) then
            ok;
            s := decrease (p, q, s)
         else
            nok
         end if
      end loop
   end var
end process

end module