module commerce (COMMERCE_TYPES, COMMERCE_PROCESSES) is

-------------------------------------------------------------------------------
-- A stock management system, composed of a central store acting as a
-- wholesale merchant between two suppliers and two local stores. This case
-- study is described in [Chirichiello-Salaun-05].
-- All transaction are organised as follows. The potential buyer (the central 
-- or one of the local stores) requests a quantity of an item (both modelled
-- by natural numbers). If a request can be fulfilled, it is followed by a
-- rendez-vous on a gate "ok", otherwise the request is followed by a
-- rendez-vous on a gate "nok".
-- The two suppliers (respectively the two local stores) do not interact with
-- each other.
-------------------------------------------------------------------------------

process MAIN [request_local: ENQUIRY,    ok_local,    nok_local: none,
              request_supplier: ENQUIRY, ok_supplier, nok_supplier: none] is
   par request_supplier, ok_supplier, nok_supplier in
      par -- two suppliers
         Supplier [request_supplier, ok_supplier, nok_supplier]
	          (stock_supplier_1)
      || Supplier [request_supplier, ok_supplier, nok_supplier]
                  (stock_supplier_2)
      end par
   ||
      par request_local, ok_local, nok_local in
         -- central store acting as wholesale merchand
         CentralStore [request_local,    ok_local,    nok_local,
                       request_supplier, ok_supplier, nok_supplier]
                      (stock_central)
      ||
         par -- two local stores
            LocalStore [request_local, ok_local, nok_local] (stock_local_1)
         || LocalStore [request_local, ok_local, nok_local] (stock_local_2)
         end par
      end par
   end par
end process

end module