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 tstart: integer
sort tend: integer
sort mode
sort value
sort state
reified sort prop:fluent
reified sort action:event
reified sort nfluent:fluent 

agent Seller, Buyer
mode Exist
value True, False, Undef
action Deliver(agent,agent,product)
prop Done(agent,action)
prop PTrue()
product CD
state Cancelled, Cond, Pending, Fulfilled, Violated

nfluent TP(prop,tstart,tend,mode)
fluent ETP(nfluent,value)
fluent Comm(state,agent,agent,nfluent,nfluent)

event AttCreateTP(prop,tstart,tend,mode)
event AttCreateComm(agent,agent,nfluent,nfluent)
event Elapse(time)
event Init()

[time]Happens(Elapse(time),time).	  

[agent1,agent2,product,action,time]
action=Deliver(agent1,agent2,product) -> 
Initiates(Deliver(agent1,agent2,product),Done(agent1,action),time). 

[prop,tstart,tend,mode,time]
 prop=PTrue() & tstart=2 & tend=3 & mode=Exist -> 
Initiates(Init(),TP(prop,tstart,tend,mode),time).

[value,time,nfluent]
value=True & nfluent=TP(PTrue(),2,3,Exist) -> 
Initiates(Init(),ETP(nfluent,value),time).

;TP1
[prop,tstart,tend,mode,time]
tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time) -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),
TP(prop,tstart,tend,mode),time).

;ETP0
[prop,tstart,tend,mode,value,nfluent,time]
value=Undef & nfluent=TP(prop,tstart,tend,mode) & 
time<(tstart-1) &  tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time)  -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),ETP(nfluent,value),time).

;CHANGE OF THE TRUTH-VALUE OF AN EXIST ETP
;ETPE4 ETP becomes True for action Deliver()
[value,agent1,agent2,product,nfluent,tstart,tend,prop,time] 
value=True & nfluent=TP(prop,tstart,tend,Exist) & 
time>=tstart-1 & time<tend & 
HoldsAt(ETP(nfluent,Undef),time) -> 
Initiates(Deliver(agent1,agent2,product),ETP(nfluent,value),time).

;ETPE5 ETP becomes False for action Elapse(tend)
[value,nfluent,tstart,tend,prop,time] 
value=False & nfluent=TP(prop,tstart,tend,Exist) & 
HoldsAt(ETP(nfluent,Undef),time) -> 
Initiates(Elapse(tend),ETP(nfluent,value),time).

;TERMINATES A REPLACED ETP
;ETP n
[value,agent1,agent2,product,nfluent,prop,tstart,tend,time]
value=Undef & nfluent=TP(prop,tstart,tend,Exist) &
prop=Done(agent1,Deliver(agent1,agent2,product)) &
HoldsAt(ETP(nfluent,Undef),time) & time>=tstart-1 & time<tend &
Happens(Deliver(agent1,agent2,product),time) -> 
Terminates(Deliver(agent1,agent2,product),ETP(nfluent,value),time).

;ETP n1
[value,nfluent,prop,tstart,tend,time]
value=Undef & nfluent=TP(prop,tstart,tend,Exist) &
HoldsAt(ETP(nfluent,Undef),time) & 
Happens(Elapse(tend),time) -> 
Terminates(Elapse(tend),ETP(nfluent,value),time).

;-----------------------------------------
;COMMITMENT AXIOMS

;C03 miss t2end<t1start
[state1,state2,agent1,agent2,product,nfluent1,nfluent2,time]
state1=Pending & agent1=Seller & agent2=Buyer & product=CD &
nfluent1=TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist) & 
nfluent2=TP(PTrue(),2,3,Exist) &
HoldsAt(ETP(nfluent1,Undef),time) & 
HoldsAt(ETP(nfluent2,True),time) &
!HoldsAt(Comm(state2,agent1,agent2,nfluent1,nfluent2),time) & 
!Happens(Deliver(agent1,agent2,product),time) ->  
Initiates(AttCreateComm(agent1,agent2,nfluent1,nfluent2),
Comm(state1,agent1,agent2,nfluent1,nfluent2),time).

;C3 Pending->Fulfilled
[state,tend,agent1,agent2,product,nfluent1,nfluent2,time] 
state=Fulfilled & agent1=Seller & agent2=Buyer & product=CD &
nfluent1=TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist) &  tend=3 &
nfluent2=TP(PTrue(),2,3,Exist) & time<tend &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) -> 
Initiates(Deliver(agent1,agent2,product),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 terminates a replaced commitment
[state,tend,agent1,agent2,product,nfluent1,nfluent2,time] 
state=Pending & agent1=Seller & agent2=Buyer & product=CD &
nfluent1=TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist) &  tend=3 &
nfluent2=TP(PTrue(),2,3,Exist) & time<tend &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) -> 
Terminates(Deliver(agent1,agent2,product),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C4 Pending->Violated
[tend,state,agent1,agent2,nfluent1,nfluent2,time] 
state=Violated & tend=3 &
nfluent1=TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist) & 
nfluent2=TP(PTrue(),2,3,Exist) &
agent1= Seller & agent2=Buyer &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) -> 
Initiates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;C5 bis terminates a replaced commitment
[tend,state,agent1,agent2,nfluent1,nfluent2,time] 
state=Pending & tend=3 &
nfluent1=TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist) & 
nfluent2=TP(PTrue(),2,3,Exist) &
agent1= Seller & agent2=Buyer &
HoldsAt(Comm(Pending,agent1,agent2,nfluent1,nfluent2),time) ->
Terminates(Elapse(tend),Comm(state,agent1,agent2,nfluent1,nfluent2),time).

;----------------------------------------------------
[fluent]!HoldsAt(fluent,0).

;HISTORY OF THE SYSTEM
Happens(Init(),0).
Happens(AttCreateTP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),0).
Happens(AttCreateComm(Seller,Buyer,TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),TP(PTrue(),2,3,Exist)),1).
Happens(Deliver(Seller,Buyer,CD),3).

completion Happens

range time 0 4
range offset 1 1
range tstart 2 2
range tend 3 3

;End of file.