option modeldiff on
option showpred off
;If on, the truth values of all predicates other than fluents and events are shown. 

load foundations/Root.e
load foundations/EC.e

sort agent
sort product
sort price: integer
sort tend: integer
sort tout: integer
sort mode
sort value
sort state
sort mtype
sort prop:fluent
sort nfluent:fluent

agent Seller, Buyer
product CD
price 1
mode Exist, Forall
value True, False, Undef 
state Cancelled, Cond, Pending, Fulfilled, Violated, Active
mtype Promise, Request, Agree, Refuse

prop DoneDeliverSellerBuyerCD, DonePayBuyerSeller1, DoneBuyerExchMsgAgree
;TP1
nfluent TPDoneDeliverSellerBuyerCD45Exist
;TP2
nfluent TPDonePayBuyerSeller167Exist
;TP3
nfluent TPDoneBuyerExchMsgAgree23Exist

fluent ETP(nfluent,value)
fluent Comm(state,agent,agent,nfluent,nfluent)
fluent Precomm(state,agent,agent,nfluent,nfluent,tout)

event ExchMsg(mtype,agent,agent,nfluent,nfluent)
event ExchMsg1(mtype,agent,agent,nfluent,nfluent,tout)

event Deliver(agent,agent,product)
event Pay(agent,agent,price)

event AttCreateTP(nfluent)
event AttCreateComm(agent,agent,nfluent,nfluent)
event AttCreatePrecomm(agent,agent,nfluent,nfluent,tout)
event AttAccceptPrecomm(agent,agent,nfluent,nfluent)
event AttCancelPrecomm(agent,agent,nfluent,nfluent)

event Elapse(time)

;------------------------------------------------------
[agent1,agent2,product,time]
agent1=Seller & agent2=Buyer & product=CD ->
Initiates(Deliver(agent1,agent2,product),DoneDeliverSellerBuyerCD(),time). 

[agent1,agent2,price,time]
agent1=Buyer & agent2=Seller & price=1 ->
Initiates(Pay(agent1,agent2,price),DonePayBuyerSeller1(),time).

[mtype,agent1,agent2,nfluent1,nfluent2,time]
mtype=Agree & agent1=Buyer & agent2=Seller & 
nfluent1=TPDonePayBuyerSeller167Exist &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist ->
Initiates(ExchMsg(mtype,agent1,agent2,nfluent1,nfluent2),DoneBuyerExchMsgAgree(),time).
	  
[time]Happens(Elapse(time),time).
;----------------------------------------------------

;TP1 axiom to create temporal propositions
[nfluent,time] 
nfluent=TPDoneDeliverSellerBuyerCD45Exist &
!HoldsAt(TPDoneDeliverSellerBuyerCD45Exist(),time) -> 
Initiates(AttCreateTP(nfluent),TPDoneDeliverSellerBuyerCD45Exist(),time).
 
[nfluent,time] 
nfluent=TPDonePayBuyerSeller167Exist &
!HoldsAt(TPDonePayBuyerSeller167Exist(),time) ->  
Initiates(AttCreateTP(nfluent),TPDonePayBuyerSeller167Exist(),time).

[nfluent,time] 
nfluent=TPDoneBuyerExchMsgAgree23Exist &
!HoldsAt(TPDoneBuyerExchMsgAgree23Exist(),time) ->  
Initiates(AttCreateTP(nfluent),TPDoneBuyerExchMsgAgree23Exist(),time).
;----------------------------------------------------

;evaluated temporal propostion axioms CASE1 mode=Exist
;ETP0
[value,nfluent,time]
value=Undef  -> 
Initiates(AttCreateTP(nfluent),ETP(nfluent,value),time).

;ETPE5 ETP becomes True nfluent=TPDoneDeliverSellerBuyerCD45Exist
[value,agent1,agent2,product,nfluent,time] 
value=True & nfluent=TPDoneDeliverSellerBuyerCD45Exist & agent1=Seller & agent2=Buyer & product=CD &
HoldsAt(ETP(nfluent,Undef),time) &
time>=4-1 & time<5 -> 
Initiates(Deliver(agent1,agent2,product),ETP(nfluent,value),time).

;ETPE5 ETP becomes True nfluent=TPDonePayBuyerSeller167Exist
[value,agent1,agent2,price,nfluent,time] 
value=True & nfluent=TPDonePayBuyerSeller167Exist & agent1=Buyer & agent2=Seller & price=1 &
HoldsAt(ETP(nfluent,Undef),time) & 
time>=6-1 & time<7 -> 
Initiates(Pay(agent1,agent2,price),ETP(nfluent,value),time).

;ETPE5 ETP becomes True nfluent=TPDoneBuyerExchMsgAgree23Exist
[value,mtype,agent1,agent2,nfluent,nfluent1,nfluent2,time] 
value=True & nfluent=TPDoneBuyerExchMsgAgree23Exist &
mtype=Agree & agent1=Buyer & agent2=Seller & 
nfluent1=TPDonePayBuyerSeller167Exist &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(ETP(nfluent,Undef),time) & 
time>=2-1 & time<3 -> 
Initiates(ExchMsg(mtype,agent1,agent2,nfluent1,nfluent2),ETP(nfluent,value),time).

;ETPE6 ETP becomes False 
[value,nfluent,tend,time] 
value=False & nfluent=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=5 -> 
Initiates(Elapse(tend),ETP(nfluent,value),time).

;ETPE6 ETP becomes False 
[value,nfluent,tend,time] 
value=False & nfluent=TPDonePayBuyerSeller167Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=7 -> 
Initiates(Elapse(tend),ETP(nfluent,value),time).

;ETPE6 ETP becomes False 
[value,nfluent,tend,time] 
value=False & nfluent=TPDoneBuyerExchMsgAgree23Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=3 -> 
Initiates(Elapse(tend),ETP(nfluent,value),time).

;TERMINATES A REPLACED ETP
;ETP1 
[value,agent1,agent2,product,nfluent,time]
value=Undef & nfluent=TPDoneDeliverSellerBuyerCD45Exist & agent1=Seller & agent2=Buyer & product=CD &
HoldsAt(ETP(nfluent,Undef),time) &
time>=4-1 & time<5  ->
Terminates(Deliver(agent1,agent2,product),ETP(nfluent,value),time).

;ETP2
[value,tend,nfluent,time]
value=Undef & nfluent=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=5 -> 
Terminates(Elapse(tend),ETP(nfluent,value),time).

;ETP1 
[value,agent1,agent2,price,nfluent,time]
value=Undef & nfluent=TPDonePayBuyerSeller167Exist & agent1=Buyer & agent2=Seller & price=1 &
HoldsAt(ETP(nfluent,Undef),time) & time>=6-1 & time<7 ->
Terminates(Pay(agent1,agent2,price),ETP(nfluent,value),time).

;ETP2
[value,tend,nfluent,time]
value=Undef & nfluent=TPDonePayBuyerSeller167Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=7 -> 
Terminates(Elapse(tend),ETP(nfluent,value),time).

;ETP1
[value,mtype,agent1,agent2,nfluent,nfluent1,nfluent2,time]
value=Undef & nfluent=TPDoneBuyerExchMsgAgree23Exist &
mtype=Agree & agent1=Buyer & agent2=Seller & 
nfluent1=TPDonePayBuyerSeller167Exist &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(ETP(nfluent,Undef),time) & time>=2-1 & time<3 -> 
Terminates(ExchMsg(mtype,agent1,agent2,nfluent1,nfluent2),ETP(nfluent,value),time).

;ETP2
[value,tend,nfluent,time]
value=Undef & nfluent=TPDoneBuyerExchMsgAgree23Exist &
HoldsAt(ETP(nfluent,Undef),time) & tend=3 -> 
Terminates(Elapse(tend),ETP(nfluent,value),time).

;---------------------------------------------------
;C01
[state1,state2,agent1,agent2,nfluent1,nfluent2,time]
state1=Cond & 
!HoldsAt(Comm(state2,agent1,agent2,nfluent1,nfluent2),time) & 
HoldsAt(ETP(nfluent1,Undef),time) & HoldsAt(ETP(nfluent2,Undef),time) ->
Initiates(AttCreateComm(agent1,agent2,nfluent1,nfluent2),
Comm(state1,agent1,agent2,nfluent1,nfluent2),time).

;C1 Cond->Pending condition=TPDoneBuyerExchMsgAgree23Exist
[state,mtype,agent1,agent2,agent3,agent4,nfluent1,nfluent2,nfluent3,nfluent4,tend,time]
state=Pending & 
nfluent2=TPDoneBuyerExchMsgAgree23Exist & tend=3 & time<tend &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time) & 
mtype=Agree & agent3=Buyer & agent4=Seller & 
nfluent3=TPDonePayBuyerSeller167Exist &
nfluent4=TPDoneDeliverSellerBuyerCD45Exist  ->
Initiates(ExchMsg(mtype,agent3,agent4,nfluent3,nfluent4),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Cond -> Pending nfluent2=TPDoneBuyerExchMsgAgree23Exist
[state,mtype,agent1,agent2,agent3,agent4,nfluent1,nfluent2,nfluent3,nfluent4,tend,time]
state=Cond & 
nfluent2=TPDoneBuyerExchMsgAgree23Exist & tend=3 & time<tend &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time) & 
mtype=Agree & agent3=Buyer & agent4=Seller & 
nfluent3=TPDonePayBuyerSeller167Exist &
nfluent4=TPDoneDeliverSellerBuyerCD45Exist ->
Terminates(ExchMsg(mtype,agent3,agent4,nfluent3,nfluent4),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C1 Cond->Pending condition=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,nfluent1,nfluent2,product,tend,time]
state=Pending & agent1=Buyer & agent2=Seller & product=CD &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist & tend=5 & time<tend &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time)  ->
Initiates(Deliver(agent2,agent1,product),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Cond -> Pending nfluent2=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,nfluent1,nfluent2,product,tend,time]
state=Cond & agent1=Buyer & agent2=Seller & product=CD &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist & tend=5 & time<tend &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time)  ->
Terminates(Deliver(agent2,agent1,product),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C2 Cond->Cancelled condition=TPDoneBuyerExchMsgAgree23Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Cancelled &  tend=3 &
nfluent2=TPDoneBuyerExchMsgAgree23Exist &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time)  ->
Initiates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Cond -> Cancelled nfluent2=TPDoneBuyerExchMsgAgree23Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Cond &  tend=3 &
nfluent2=TPDoneBuyerExchMsgAgree23Exist &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time)  ->
Terminates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C2 Cond->Cancelled condition=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Cancelled &  tend=5 &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time) ->
Initiates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5.2 Cond -> Cancelled nfluent2=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Cond &  tend=5 &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Cond,agent1,agent2,nfluent1,nfluent2),time) ->
Terminates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C3 Pending->Fulfilled nfluent1=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,product,nfluent1,nfluent2,tend,time]
state=Fulfilled & agent1=Seller & agent2=Buyer & product=CD &
nfluent1=TPDoneDeliverSellerBuyerCD45Exist & tend=5 & time<tend &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time)  ->
Initiates(Deliver(agent1,agent2,product),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Pending -> Fulfilled nfluent1=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,product,nfluent1,nfluent2,tend,time]
state=Pending & agent1=Seller & agent2=Buyer & product=CD &
nfluent1=TPDoneDeliverSellerBuyerCD45Exist & tend=5 & time<tend &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time)  ->
Terminates(Deliver(agent1,agent2,product),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C3 Pending->Fulfilled nfluent1=TPDonePayBuyerSeller167Exist
[state,agent1,agent2,price,nfluent1,nfluent2,tend,time]
state=Fulfilled & agent1=Buyer & agent2=Seller & price=1 &
nfluent1=TPDonePayBuyerSeller167Exist & tend=7 & time<tend &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) ->
Initiates(Pay(agent1,agent2,price),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Pending->Fulfilled nfluent1=TPDonePayBuyerSeller167Exist
[state,agent1,agent2,price,nfluent1,nfluent2,tend,time]
state=Pending & agent1=Buyer & agent2=Seller & price=1 &
nfluent1=TPDonePayBuyerSeller167Exist & tend=7 & time<tend &
nfluent2=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) ->
Terminates(Pay(agent1,agent2,price),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C4 Pending->Violated nfluent1=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,tend,nfluent1,nfluent2,time]
state=Violated & agent1=Seller & agent2=Buyer & tend=5 &
nfluent1=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) ->
Initiates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 Pending -> Violated nfluent1=TPDoneDeliverSellerBuyerCD45Exist
[state,agent1,agent2,tend,nfluent1,nfluent2,time]
state=Pending & agent1=Seller & agent2=Buyer & tend=5 &
nfluent1=TPDoneDeliverSellerBuyerCD45Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) ->
Terminates(Elapse(tend),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C4 Pending->Violated nfluent1=TPDonePayBuyerSeller167Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Violated & agent1=Buyer & agent2=Seller & tend=7 &
nfluent1=TPDonePayBuyerSeller167Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time)  ->
Initiates(Elapse(tend),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5.4 Pending->Violated nfluent1=TPDonePayBuyerSeller167Exist
[state,agent1,agent2,nfluent1,nfluent2,tend,time]
state=Pending & agent1=Buyer & agent2=Seller & tend=7 &
nfluent1=TPDonePayBuyerSeller167Exist &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time)  ->
Terminates(Elapse(tend),
Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;PRECOMMITMENT AXIOMS

;P1
[state,state2,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Active & tout>time &
!HoldsAt(Precomm(state2,agent1,agent2,nfluent1,nfluent2,tout),time) ->  
Initiates(AttCreatePrecomm(agent1,agent2,nfluent1,nfluent2,tout),
Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;P2
[agent1,agent2,nfluent1,nfluent2,time]
 Happens(AttAccceptPrecomm(agent1,agent2,nfluent1,nfluent2),time) & 
 ({tout} HoldsAt(Precomm(Active,agent1,agent2,nfluent1,nfluent2,tout),time) & time<tout)  ->
 Happens(AttCreateComm(agent1,agent2,nfluent1,nfluent2),time).

;P3
[state,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Active &
HoldsAt(Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time) & time<tout  ->
Terminates(AttAccceptPrecomm(agent1,agent2,nfluent1,nfluent2),
Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;P4
[state,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Cancelled &
HoldsAt(Precomm(Active,agent1,agent2,nfluent1,nfluent2,tout),time) & time<tout ->  
Initiates(AttCancelPrecomm(agent1,agent2,nfluent1,nfluent2),
Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;P5
[state,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Active &
HoldsAt(Precomm(Active,agent1,agent2,nfluent1,nfluent2,tout),time) & time<tout -> 
Terminates(AttCancelPrecomm(agent1,agent2,nfluent1,nfluent2),
Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;P6
[state,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Cancelled &
HoldsAt(Precomm(Active,agent1,agent2,nfluent1,nfluent2,tout),time)  ->  
Initiates(Elapse(tout),Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;P7
[state,agent1,agent2,nfluent1,nfluent2,tout,time]
state=Active &
HoldsAt(Precomm(Active,agent1,agent2,nfluent1,nfluent2,tout),time) ->
Terminates(Elapse(tout),Precomm(state,agent1,agent2,nfluent1,nfluent2,tout),time).

;AXIOM PRO
 [agent1,agent2,nfluent1,nfluent2,time]
 Happens(ExchMsg(Promise,agent1,agent2,nfluent1,nfluent2),time) ->
 Happens(AttCreateComm(agent1,agent2,nfluent1,nfluent2),time).
 
;AXIOM REQ
 [agent1,agent2,nfluent1,nfluent2,tout,time]
 Happens(ExchMsg1(Request,agent1,agent2,nfluent1,nfluent2,tout),time) ->
 Happens(AttCreatePrecomm(agent2,agent1,nfluent1,nfluent2,tout),time).
 
;AXIOM AGREE
[agent1,agent2,nfluent1,nfluent2,time]
Happens(ExchMsg(Agree,agent1,agent2,nfluent1,nfluent2),time) ->
Happens(AttAccceptPrecomm(agent1,agent2,nfluent1,nfluent2),time).

;AXIOM REFUSE
[agent1,agent2,nfluent1,nfluent2,time]
Happens(ExchMsg(Refuse,agent1,agent2,nfluent1,nfluent2),time) ->
Happens(AttCancelPrecomm(agent1,agent2,nfluent1,nfluent2),time).

[fluent]!HoldsAt(fluent,0).
!HoldsAt(DoneDeliverSellerBuyerCD(),0).
!HoldsAt(DonePayBuyerSeller1(),0).
!HoldsAt(DoneBuyerExchMsgAgree(),0).
!HoldsAt(TPDoneDeliverSellerBuyerCD45Exist(),0).
!HoldsAt(TPDonePayBuyerSeller167Exist(),0).
!HoldsAt(TPDoneBuyerExchMsgAgree23Exist(),0).

;HISTORY OF THE SYSTEM
 Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist),0).
 Happens(AttCreateTP(TPDonePayBuyerSeller167Exist),0).
 Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist),0).
 Happens(ExchMsg(Promise,Seller,Buyer,TPDoneDeliverSellerBuyerCD45Exist,TPDoneBuyerExchMsgAgree23Exist),1).
 Happens(ExchMsg1(Request,Seller,Buyer,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist,3),1).
 Happens(ExchMsg(Refuse,Buyer,Seller,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist),2).
 ;Happens(ExchMsg(Agree,Buyer,Seller,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist),2).
 ;Happens(Deliver(Seller,Buyer,CD),4).
 ;Happens(Pay(Buyer,Seller,1),7).
  
completion Happens

range time 0 8
range offset 1 1
range price 1 1
range tend 3 7
range tout 3 3

;End of file.