:- module Pur.

:- imports  import Ord; 
            import Shp; 
            import Pay.
 
:- role-identification
   Pur.Customer is Ord.Buyer, Shp.Receiver, Pay.Payer;
   Pur.Merchant is Ord.Seller, Shp.Sender, Pay.Payee;
   Pur.Shipper is Shp.Shipper;
   Pur.Gateway is Pay.Gateway.

:- data-flow
   Shp.reqForshipOptions.Item uses Ord.accept.ItemID if T;
   Pay.authReq.Amount uses Ord.accept.ItemPrice if T.

:- commitment-condition
   Shp.shipment(item) means Ord.deliver(item);
   Shp.authOK(token, amount) means Ord.payment(amount).

:- event-order
   Pay.authOK before Shp.shipOrder.