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
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)
product CD

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

event AttCreateTP(prop,tstart,tend,mode)
event Elapse(time)

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

[agent1,agent2,product,action,time]
action=Deliver(agent1,agent2,product) -> 
Initiates(Deliver(agent1,agent2,product),Done(agent1,action),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).

;ETPE1
[prop,tstart,tend,mode,value,nfluent,time1,event]
value=True & nfluent=TP(prop,tstart,tend,mode) & mode=Exist &
prop=Done(Seller,Deliver(Seller,Buyer,CD)) &
event=Deliver(Seller,Buyer,CD) &
tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time1) &
time1>=(tstart-1) & time1<tend &
({time2} Happens(event,time2) & time2>=tstart-1 & time2<=time1) -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),ETP(nfluent,value),time1).

;with & !({event} Happens(event,time) & Initiates(event,prop,time)) and without prop=Done(Seller....) infinite

;ETPE2
[prop,tstart,tend,mode,value,nfluent,time1,event]
value=Undef & nfluent=TP(prop,tstart,tend,mode) & mode=Exist &
prop=Done(Seller,Deliver(Seller,Buyer,CD)) &
event=Deliver(Seller,Buyer,CD) &
tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time1) &
time1>=(tstart-1) & time1<tend &
!({time2} Happens(event,time2) & time2>=tstart-1 & time2<=time1) -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),ETP(nfluent,value),time1).

;ETPE3
[prop,tstart,tend,mode,value,nfluent,time1,event]
value=True & nfluent=TP(prop,tstart,tend,mode) & mode=Exist &
prop=Done(Seller,Deliver(Seller,Buyer,CD)) &
event=Deliver(Seller,Buyer,CD) &
tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time1) &
time1>=tend &
({time2} Happens(event,time2) & time2>=tstart-1 & time2<tend) -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),ETP(nfluent,value),time1).

;ETPE4
[prop,tstart,tend,mode,value,nfluent,time1,event]
value=False & nfluent=TP(prop,tstart,tend,mode) & mode=Exist &
prop=Done(Seller,Deliver(Seller,Buyer,CD)) &
event=Deliver(Seller,Buyer,CD) &
tstart<=tend & !HoldsAt(TP(prop,tstart,tend,mode),time1) &
time1>=tend &
!({time2} Happens(event,time2) & time2>=tstart-1 & time2<tend) -> 
Initiates(AttCreateTP(prop,tstart,tend,mode),ETP(nfluent,value),time1).

;CHANGE OF THE TRUTH-VALUE OF AN EXIST ETP
;ETPE5 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).

;ETPE6 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
;ETP1
[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).

;ETP2
[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).

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

;HISTORY OF THE SYSTEM
Happens(AttCreateTP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),3).
Happens(Deliver(Seller,Buyer,CD),2).

completion Happens

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

;End of file.