:- include 'protocol_ontology_simple.ncl'. :- sorts Slot >> PriceRequestID; Slot >> PriceResponseID; Slot >> Currency1; Slot >> Currency2; Slot >> Amount1; Slot >> Amount2; Slot >> Rate; Slot >> ExecConfReq; Slot >> TTL; Slot >> Result; Slot >> Direction; Role >> Taker; Role >> Maker. :- objects priceRequest(Taker,Maker,PriceRequestID,Currency1,Currency2,Amount1) :: Message; cancelPriceRequest(Taker,Maker,PriceRequestID) :: Message; priceResponse(Maker,Taker,PriceResponseID,PriceRequestID,Result,ExecConfReq,TTL,Rate) :: Message; cancelPrice(Maker,Taker,PriceResponseID) :: Message; priceAcceptance(Taker,Maker,PriceResponseID,Direction) :: Message; nothingDone(Taker,Maker,PriceResponseID) :: Message; priceAcceptanceAck(Maker,Taker,PriceResponseID) :: Message; executionConfirmation(Maker,Taker,PriceResponseID,Result) :: Message; executionConfirmationAck(Taker,Maker,PriceResponseID) :: Message; ttlExpired(PriceResponseID) :: Message; priceResponsePrecond(PriceResponseID) :: Condition; priceResponseCond(PriceResponseID) :: Condition; priceAcceptancePrecond(PriceResponseID) :: Condition; priceAcceptanceCond(PriceResponseID) :: Condition; execConfPrecond(PriceResponseID) :: Condition; execConfCond(PriceResponseID) :: Condition; pay(PriceResponseID,Amount2) :: Condition; pay(PriceResponseID,Amount1) :: Condition; reqID1 :: PriceRequestID; resID1 :: PriceResponseID; EUR :: Currency1; USD :: Currency2; 1000 :: Amount1; 1200 :: Amount2; 1.2 :: Rate; 5 :: TTL; YES, NO :: ExecConfReq; DONE, FAILED :: Result; TakerBuys, TakerSells :: Direction; myTaker :: Taker; myMaker :: Maker. :- variables reqID :: PriceRequestID; resID, resIDa, resIDb, resIDc :: PriceResponseID; m :: Maker; t :: Taker; cur1 :: Currency1; cur2 :: Currency2; amt1 :: Amount1; amt2 :: Amount2; rate, rate1, rate2 :: Rate; execConfReq, execConfReq1, execConfReq2 :: ExecConfReq; res, res1, res2 :: Result; dir, dir1, dir2 :: Direction; ttl, ttl1, ttl2 :: TTL. %% request can be made only once %% nonexecutable act(priceRequest(t,m,reqID,cur1,cur2,amt1)) if fl(priceRequest(t,m,reqID,cur1,cur2,amt1)). %% many responses can be sent once request has happened %% until nothingDone or acceptance happens and it is confirmed %% only one response with a resID is allowed nonexecutable act(priceResponse(m,t,resID,reqID,res,execConfReq,ttl,rate)) if -[\/cur1 \/cur2 \/amt1 | fl(priceRequest(t,m,reqID,cur1,cur2,amt1))] ++ ((fl(nothingDone(t,m,resIDa)) ++ fl(priceAcceptance(t,m,resIDb,dir))) & -(fl(executionConfirmation(m,t,resIDb,FAILED)) & fl(executionConfirmationAck(t,m,resIDb))) ) ++ act(priceResponse(m,t,resID,reqID,res2,execConfReq2,ttl2,rate2)) ++ fl(priceResponse(m,t,resID,reqID,res,execConfReq,ttl,rate)) where res<>res2 ++ execConfReq<>execConfReq2 ++ ttl<>ttl2 ++ rate<>rate2. %%TTL can expire anytime after the response nonexecutable act(ttlExpired(resID)) if -[\/reqID \/res \/execConfReq | fl(priceResponse(m,t,resID,reqID,res,execConfReq,ttl,rate))]. %% request can be canceled if response has not happened %% nonexecutable act(cancelPriceRequest(t,m,reqID)) if -[\/cur1 \/cur2 \/amt1 | fl(priceRequest(t,m,reqID,cur1,cur2,amt1))] ++ fl(priceResponse(m,t,resID,reqID,res,execConfReq,ttl,rate)) ++ fl(cancelPriceRequest(t,m,reqID)). %% price can be accepted if it is received successfully %% and has not been rejected %% price can be accepted in only one direction nonexecutable act(priceAcceptance(t,m,resID,dir)) if -[\/reqID \/execConfReq | fl(priceResponse(m,t,resID,reqID,DONE,execConfReq,ttl,rate))] ++ fl(priceAcceptance(t,m,resID,dir1)) ++ act(priceAcceptance(t,m,resID,dir2)) ++ fl(nothingDone(t,m,resID)) where dir<>dir2. %% price can be rejected if it is received successfully and %% has not been accepted nonexecutable act(nothingDone(t,m,resID)) if -[\/reqID \/execConfReq | fl(priceResponse(m,t,resID,reqID,DONE,execConfReq,ttl,rate))] ++ fl(priceAcceptance(t,m,resID,dir)) ++ fl(nothingDone(t,m,resID)). %% price cannot be accpted and rejected simultaneously. nonexecutable act(nothingDone(t,m,resID)) if act(priceAcceptance(t,m,resID,dir)). %% price can be canceled if it has not been accepted %% nonexecutable act(cancelPrice(m,t,resID)) if -[\/reqID \/execConfReq | fl(priceResponse(m,t,resID,reqID,DONE,execConfReq,ttl,rate))] ++ fl(priceAcceptance(t,m,resID,dir)) ++ fl(cancelPrice(m,t,resID)). %% price cancellation cancels the commitment made at priceResponse %% %% in the case that the confirmation is not required %% caused cancel(cc(m,t,priceResponsePrecond(resID),priceResponseCond(resID))) if act(cancelPrice(m,t,resID)) & fl(priceResponse(m,t,resID,reqID,DONE,NO,ttl,rate)). %% price acceptance is acked if execution confirmation is not required %% nonexecutable act(priceAcceptanceAck(m,t,resID)) if fl(priceResponse(m,t,resID,reqID,res,YES,ttl,rate)) ++ -[\/dir | fl(priceAcceptance(t,m,resID,dir))] ++ fl(priceAcceptanceAck(m,t,resID)). %% execution is confirmed if it is required to do so %% %% and it is either DONE or FAILED nonexecutable act(executionConfirmation(m,t,resID,res)) if -[\/reqID \/res1 | fl(priceResponse(m,t,resID,reqID,res1,YES,ttl,rate))] ++ -[\/dir | fl(priceAcceptance(t,m,resID,dir))] ++ fl(executionConfirmation(m,t,resID,res2)) ++ act(executionConfirmation(m,t,resID,res2)) where res<>res2. %% the confirmation is acked if it is received %% nonexecutable act(executionConfirmationAck(t,m,resID)) if -[\/res | fl(executionConfirmation(m,t,resID,res))] ++ fl(executionConfirmationAck(t,m,resID)). %% commitment CC0 %% caused create(cc(m,t,priceResponsePrecond(resID),priceResponseCond(resID))) if act(priceResponse(m,t,resID,reqID,DONE,NO,ttl,rate)). caused cond(priceResponsePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & -fl(ttlExpired(resID)) & create(cc(t,m,T,pay(resID,amt2))). caused cond(priceResponsePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & -fl(ttlExpired(resID)) & create(cc(t,m,T,pay(resID,amt1))). caused cond(priceResponseCond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(m,t,T,pay(resID,amt1))). caused cond(priceResponseCond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(m,t,T,pay(resID,amt2))). %% commitment CC1 %% caused create(cc(t,m,priceAcceptancePrecond(resID), priceAcceptanceCond(resID))) if act(priceAcceptance(t,m,resID,dir)) & fl(priceResponse(m,t,resID,reqID,DONE,NO,ttl,rate)) & -fl(ttlExpired(resID)). caused cond(priceAcceptancePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(m,t,T,pay(resID,amt1))). caused cond(priceAcceptancePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(m,t,T,pay(resID,amt2))). caused cond(priceAcceptanceCond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(t,m,T,pay(resID,amt2))). caused cond(priceAcceptanceCond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(t,m,T,pay(resID,amt1))). %% commitment CC2 % caused create(cc(t,m,priceAcceptancePrecond(resID), priceAcceptanceCond(resID))) if act(priceAcceptance(t,m,resID,dir)) & fl(priceResponse(m,t,resID,reqID,DONE,YES,ttl,rate)) & fl(executionConfirmation(m,t,resID,DONE)) & -fl(ttlExpired(resID)). caused cond(priceAcceptancePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(m,t,T,pay(resID,amt1))). caused cond(priceAcceptancePrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(m,t,T,pay(resID,amt2))). caused cond(priceAcceptanceCond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(t,m,T,pay(resID,amt2))). caused cond(priceAcceptanceCond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(t,m,T,pay(resID,amt1))). %% commitment CC3 %% caused create(cc(m,t,execConfPrecond(resID),execConfCond(resID))) if act(executionConfirmation(m,t,resID,DONE)). caused cond(execConfPrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(t,m,T,pay(resID,amt2))). caused cond(execConfPrecond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(t,m,T,pay(resID,amt1))). caused cond(execConfCond(resID)) if fl(priceAcceptance(t,m,resID,TakerBuys)) & create(cc(m,t,T,pay(resID,amt1))). caused cond(execConfCond(resID)) if fl(priceAcceptance(t,m,resID,TakerSells)) & create(cc(m,t,T,pay(resID,amt2))). %% causation of conditions %% caused create(cc(m,t,T,pay(resID,amt1))) if act(priceAcceptanceAck(m,t,resID)) & fl(priceAcceptance(t,m,resID,TakerBuys)). caused create(cc(m,t,T,pay(resID,amt2))) if act(priceAcceptanceAck(m,t,resID)) & fl(priceAcceptance(t,m,resID,TakerSells)). caused create(cc(t,m,T,pay(resID,amt1))) if act(executionConfirmationAck(t,m,resID)) & fl(executionConfirmation(m,t,resID,DONE)) & fl(priceAcceptance(t,m,resID,TakerSells)). caused create(cc(t,m,T,pay(resID,amt2))) if act(executionConfirmationAck(t,m,resID)) & fl(executionConfirmation(m,t,resID,DONE)) & fl(priceAcceptance(t,m,resID,TakerBuys)). %% confirmation not required scenario1 :- query label :: 51; maxstep :: 6; 0: initial; maxstep: comm(cc(t,m,T,priceAcceptanceCond(resID))) & comm(cc(m,t,T,pay(resID,amt2))) & fl(priceAcceptance(t,m,resID,TakerSells)). %% confirmation not required scenario2 :- query label :: 52; maxstep :: 6; 0: initial; maxstep: comm(cc(t,m,T,priceAcceptanceCond(resID))) & comm(cc(m,t,T,pay(resID,amt1))) & fl(priceAcceptance(t,m,resID,TakerBuys)). %% confirmation required scenario1 :- query label :: 53; maxstep :: 6; 0: initial; maxstep: comm(cc(m,t,T,execConfCond(resID))) & comm(cc(t,m,T,pay(resID,amt2))) & fl(priceAcceptance(t,m,resID,TakerBuys)). %% confirmation required scenario2 :- query label :: 54; maxstep :: 6; 0: initial; maxstep: comm(cc(m,t,T,execConfCond(resID))) & comm(cc(t,m,T,pay(resID,amt1))) & fl(priceAcceptance(t,m,resID,TakerSells)). :- query label :: 4; maxstep :: 2; 0: initial; maxstep: fl(priceResponse(m,t,resID,reqID,DONE,NO,ttl,rate)). :- query label :: 3; maxstep :: 3; 0: initial; maxstep: fl(priceAcceptance(t,m,resID,TakerSells)). :- query label :: 2; maxstep :: 4; 0: initial; maxstep: fl(priceAcceptanceAck(m,t,resID)). %% this should have no solutions :- query label :: 1; maxstep :: 6; 0: initial; maxstep: fl(priceAcceptanceAck(m,t,resID)) & fl(executionConfirmation(m,t,resID,res)). %% only one party committed, should have no solutions :- query label :: 61; maxstep :: 6; 0: initial; maxstep: (comm(cc(t,m,T,p)) & -[\/q | comm(cc(m,t,T,q))]) ++ (comm(cc(m,t,T,p)) & -[\/q | comm(cc(t,m,T,q))]).