%:- module Pay.

:- include 'upper-onto.ncl'.

:- sorts
  Slot >> CardNO;  
  Slot >> ExpDate;
  Slot >> Amount;  
  Slot >> Token;
  
  Role >> Payer;  
  Role >> Payee; 
  Role >> Gateway.

:- objects
  paymentInfo(Payer,Payee,CardNO,ExpDate) :: Message;
  authReq(Payee,Gateway,CardNO,ExpDate,Amount) :: Message;
  authOK(Gateway,Payee,Token,Amount) :: Message;  
  authNOK(Gateway,Payee,Amount) :: Message;  
  receipt(Payee,Payer,Amount) :: Message;  
  captureReq(Payee,Gateway,Token) :: Message;  
  captured(Gateway,Payee,Amount) :: Message;  
  
  reqFund(Token) :: Condition;  
  fund(Amount) :: Condition;
  
  Pe :: Payee;  
  Pr :: Payer; 
  G :: Gateway;
  
  myCardNO :: CardNO;
  myExpDate :: ExpDate;
  myAmount :: Amount;
  myToken :: Token.
  
:- variables
  cardNO :: CardNO;  
  expDate :: ExpDate;
  amount :: Amount;
  token :: Token.


nonexecutable act(paymentInfo(Pr,Pe,cardNO,expDate)) if
fl(paymentInfo(Pr,Pe,cardNO,expDate)).

nonexecutable act(authReq(Pe,G,cardNO,expDate,amount)) if
-fl(paymentInfo(Pr,Pe,cardNO,expDate)) ++ fl(authReq(Pe,G,cardNO,expDate,amount)).

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

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

nonexecutable act(authNOK(G,Pe,amount)) if act(authOK(G,Pe,token,amount)).

act(authOK(G,Pe,token,amount)) causes
create(cc(G,Pe,reqFund(token),fund(amount))).

nonexecutable act(receipt(Pe,Pr,amount)) if
-fl(authOK(G,Pe,token,amount)) ++ fl(receipt(Pe,Pr,amount)).

nonexecutable act(captureReq(Pe,G,token)) if
-fl(receipt(Pe,Pr,amount)) ++ fl(captureReq(Pe,G,token)).

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

nonexecutable act(captured(G,Pe,amount)) if
-fl(captureReq(Pe,G,token)) ++ fl(captured(G,Pe,amount)).

act(captured(G,Pe,amount)) causes cond(fund(amount)).

:- query
label :: 5;  maxstep :: 6;  0: initial;
maxstep: fl(captured(G,Pe,amount)) ++ fl(authNOK(G,Pe,amount)).