:- include 'upper-onto.ncl'.

:- sorts
  Slot >> ItemID;  
  Slot >> ItemPrice;
  Slot >> ShipAddress;
  Slot >> ShipOption;  
  Slot >> ShipperQuote;
  Slot >> SenderQuote;
  Slot >> CardNO;  
  Slot >> ExpDate;
  Slot >> Token;
  

  Role >> Customer;  
  Role >> Merchant;
  Role >> Shipper; 
  Role >> Gateway.


:- objects
  reqForQuote(Customer,Merchant,ItemID) :: Message;
  quote(Merchant,Customer,ItemID,ItemPrice) :: Message;
  accept(Customer,Merchant,ItemID,ItemPrice) :: Message;
  reject(Customer,Merchant,ItemID,ItemPrice) :: Message;
  shipInfo(Customer,Merchant,ShipAddress) :: Message;
  reqForShipOptions(Merchant,Shipper,ShipAddress,ItemID) :: Message;
  shipperOptionQuote(Shipper,Merchant,ShipOption,ShipperQuote) :: Message;
  senderOptionQuote(Merchant,Customer,ShipOption,SenderQuote) :: Message;
  chooseOption(Customer,Merchant,ShipOption,SenderQuote) :: Message;
  shipOrder(Merchant,Shipper,ItemID,ShipOption,ShipperQuote) :: Message;
  shipment(Shipper,Customer,ItemID) :: Message;
  paymentInfo(Customer,Merchant,CardNO,ExpDate) :: Message;
  authReq(Merchant,Gateway,CardNO,ExpDate,ItemPrice) :: Message;
  authOK(Gateway,Merchant,Token,ItemPrice) :: Message;  
  authNOK(Gateway,Merchant,ItemPrice) :: Message;  
  receipt(Merchant,Customer,ItemPrice) :: Message;  
  captureReq(Merchant,Gateway,Token) :: Message;  
  captured(Gateway,Merchant,ItemPrice) :: Message;  

  
  deliver(ItemID) :: Condition;  
  payment(ItemPrice) :: Condition;
  payShipping :: Condition;  
  shipping(ItemID) :: Condition;
  payShippingCharge :: Condition;  
  shipping(ItemID) :: Condition;
  reqFund(Token) :: Condition;  
  fund(ItemPrice) :: Condition;
  
  c :: Customer;  
  m :: Merchant;
  Sh :: Shipper; 
  G :: Gateway;
  

  myItem :: ItemID;  
  myPrice :: ItemPrice;
  myShipAddress :: ShipAddress;
  myShipOption :: ShipOption;
  myShipperQuote :: ShipperQuote;
  mySenderQuote :: SenderQuote;
  myCardNO :: CardNO;
  myExpDate :: ExpDate;
  myToken :: Token.
  
:- variables
  itemID :: ItemID;  
  itemPrice :: ItemPrice;
  shipAddress :: ShipAddress;
  shipOption :: ShipOption;
  shipperQuote :: ShipperQuote;
  senderQuote :: SenderQuote;
  cardNO :: CardNO;  
  expDate :: ExpDate;
  token :: Token.


nonexecutable act(reqForQuote(c,m,itemID)) if
fl(reqForQuote(c,m,itemID)).

nonexecutable act(quote(m,c,itemID,itemPrice)) if 
-fl(reqForQuote(c,m,itemID)) ++  fl(quote(m,c,itemID,itemPrice)).

nonexecutable act(accept(c,m,itemID,itemPrice)) if 
-fl(quote(m,c,itemID,itemPrice)) ++ 
fl(accept(c,m,itemID,itemPrice)) ++
fl(reject(c,m,itemID,itemPrice)). 

nonexecutable act(reject(c,m,itemID,itemPrice)) if 
-fl(quote(m,c,itemID,itemPrice)) ++ 
fl(accept(c,m,itemID,itemPrice)) ++
fl(reject(c,m,itemID,itemPrice)). 

nonexecutable act(reject(c,m,itemID,itemPrice)) if 
act(accept(c,m,itemID,itemPrice)).

act(quote(m,c,itemID,itemPrice)) causes 
create(cc(m,c,payment(itemPrice),deliver(itemID))).

act(accept(c,m,itemID,itemPrice)) causes create(
cc(c,m,deliver(itemID),payment(itemPrice))). 


nonexecutable act(shipInfo(c,m,shipAddress)) if
fl(shipInfo(c,m,shipAddress)).

nonexecutable act(reqForShipOptions(m,Sh,shipAddress,itemID)) if
-fl(shipInfo(c,m,shipAddress)) ++  fl(reqForShipOptions(m,Sh,shipAddress,itemID)).

nonexecutable act(shipperOptionQuote(Sh,m,shipOption,shipperQuote)) if
-fl(reqForShipOptions(m,Sh,shipAddress,itemID)) ++ fl(shipperOptionQuote(Sh,m,shipOption,shipperQuote)).

act(shipperOptionQuote(Sh,m,shipOption,shipperQuote)) causes
create(cc(Sh,m,payShipping,shipping(itemID))).

nonexecutable act(senderOptionQuote(m,c,shipOption,senderQuote)) if
-fl(shipperOptionQuote(Sh,m,shipOption,shipperQuote)) ++ fl(senderOptionQuote(m,c,shipOption,senderQuote)).

act(senderOptionQuote(m,c,shipOption,senderQuote)) causes
create(cc(Sh,m,payShippingCharge,shipping(itemID))).

nonexecutable act(chooseOption(c,m,shipOption,senderQuote)) if
-fl(senderOptionQuote(m,c,shipOption,senderQuote)) ++ fl(chooseOption(c,m,shipOption,senderQuote)).

act(chooseOption(c,m,shipOption,senderQuote)) causes
create(cc(c,m,shipping(itemID),payShippingCharge)).

nonexecutable act(shipOrder(m,Sh,itemID,shipOption,shipperQuote)) if
-fl(chooseOption(c,m,shipOption,senderQuote)) ++ fl(shipOrder(m,Sh,itemID,shipOption,shipperQuote)).

act(shipOrder(m,Sh,itemID,shipOption,shipperQuote)) causes
create(cc(m,Sh,shipping(itemID),payShipping)).

nonexecutable act(shipment(Sh,c,itemID)) if
-fl(shipOrder(m,Sh,itemID,shipOption,shipperQuote)) ++ fl(shipment(Sh,c,itemID)).

act(shipment(Sh,c,itemID)) causes cond(shipping(itemID)).


nonexecutable act(paymentInfo(c,m,cardNO,expDate)) if
fl(paymentInfo(c,m,cardNO,expDate)).

nonexecutable act(authReq(m,G,cardNO,expDate,itemPrice)) if
-fl(paymentInfo(c,m,cardNO,expDate)) ++ fl(authReq(m,G,cardNO,expDate,itemPrice)).

nonexecutable act(authOK(G,m,token,itemPrice)) if
-fl(authReq(m,G,cardNO,expDate,itemPrice)) ++ fl(authOK(G,m,token,itemPrice)) 
++ fl(authNOK(G,m,itemPrice)).

nonexecutable act(authNOK(G,m,itemPrice)) if
-fl(authReq(m,G,cardNO,expDate,itemPrice)) ++ fl(authOK(G,m,token,itemPrice)) 
++ fl(authNOK(G,m,itemPrice)).

nonexecutable act(authNOK(G,m,itemPrice)) if act(authOK(G,m,token,itemPrice)).

act(authOK(G,m,token,itemPrice)) causes
create(cc(G,m,reqFund(token),fund(itemPrice))).

nonexecutable act(receipt(m,c,itemPrice)) if
-fl(authOK(G,m,token,itemPrice)) ++ fl(receipt(m,c,itemPrice)).

nonexecutable act(captureReq(m,G,token)) if
-fl(receipt(m,c,itemPrice)) ++ fl(captureReq(m,G,token)).

act(captureReq(m,G,token)) causes cond(reqFund(token)).

nonexecutable act(captured(G,m,itemPrice)) if
-fl(captureReq(m,G,token)) ++ fl(captured(G,m,itemPrice)).

act(captured(G,m,itemPrice)) causes cond(fund(itemPrice)).

%%%%% rules added via composition %%%%
nonexecutable act(reqForShipOptions(m,Sh,shipAddress,itemID)) if
-act(accept(c,m,itemID,itemPrice)) &
-fl(accept(c,m,itemID,itemPrice)).

nonexecutable act(authReq(m,G,cardNO,expDate,itemPrice)) if
-act(accept(c,m,itemID,itemPrice)) &
-fl(accept(c,m,itemID,itemPrice)).

caused cond(deliver(itemID)) if act(shipment(Sh,c,itemID)).

caused cond(payment(itemPrice)) if act(authOK(G,m,token,itemPrice)).

nonexecutable act(shipOrder(m,Sh,itemID,shipOption,shipperQuote)) if
-fl(authOK(G,m,token,itemPrice)).


:- query
label :: 5;  maxstep :: 9;  0: initial;
maxstep: fl(shipment(Sh,c,itemID)) & fl(captured(G,m,itemPrice)).