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
reified sort nfluent:fluent
sort role
sort astate
sort aid
sort nid
sort tinit: integer
reified sort iaction:event
sort mtype
sort tpfluent:fluent
reified sort nevent:event
sort source
reified sort npower:fluent
sort state
sort value
sort tend: integer

agent Bob, Carl, Luke, IntSystem
role Auctioneer, Participant
astate Reg,Open
aid 01
nid N1
mtype Declare
source SNorm, Sanction
state Pending, Fulfilled, Violated
value True, Undef, False

tpfluent TPDoneOpenAuction0145Exist
tpfluent TPTrue
tpfluent TPDonePayBobAuctionHouse167Exist

npower Power(agent,iaction)
fluent Context(iaction)

fluent HasRole(agent,role,nfluent)
fluent RoleOf(role,nfluent)
iaction AssignRole(agent,agent,role,nfluent)

nfluent Auction(aid,astate,tinit)
;event CreateAuction(aid,tinit)
iaction OpenAuction(aid)

iaction DecTrust(agent)

event ExchMsgD(mtype,agent,agent,iaction)
event Empower(agent,agent,iaction)
event AttCreateComm(agent,agent,tpfluent,tpfluent,source,nid)

event AttCreateTP(tpfluent)
fluent ETP(tpfluent,value)

fluent Norm(nid,agent,agent,tpfluent,tpfluent,nevent,tpfluent)

fluent Comm(state,agent,agent,tpfluent,tpfluent,source,nid)

nevent Elapse(time)

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

;AXIOM DECLARE 
[agent1,agent2,iaction,time]
Happens(ExchMsgD(Declare,agent1,agent2,iaction),time) & 
HoldsAt(Power(agent1,iaction),time) & HoldsAt(Context(iaction),time) -> 
Happens(iaction,time).

;Axiom Power1
[agent1,agent2,iaction,time]
Initiates(Empower(agent1,agent2,iaction),Power(agent2,iaction),time).

;axiom Init Context OpenAuction
[time1,time,iaction,aid]
time1=0 & iaction=OpenAuction(aid) ->
Initiates(Elapse(time1),Context(iaction),time).

;axiom Init Context AssignRole
[iaction,agent1,role,nfluent,tinit,aid,time1,time]
iaction=AssignRole(IntSystem,agent1,role,nfluent) & time1=0 & agent1!=IntSystem &
nfluent=Auction(aid,Reg,tinit) & role=Auctioneer ->
Initiates(Elapse(time1),Context(iaction),time).

;axiom Init Context AssignRole
[iaction,agent1,role,nfluent,tinit,aid,time1,time]
iaction=AssignRole(IntSystem,agent1,role,nfluent) & time1=0 & agent1!=IntSystem &
nfluent=Auction(aid,Reg,tinit) & role=Participant ->
Initiates(Elapse(time1),Context(iaction),time).

;axiom Init Power AssignRole
[iaction,agent1,agent2,role,nfluent,tinit,aid,time1,time]
iaction=AssignRole(agent1,agent2,role,nfluent) & agent1=IntSystem & time1=0 & agent2!=IntSystem &
nfluent=Auction(aid,Reg,tinit) & role=Auctioneer ->
Initiates(Elapse(time1),Power(agent1,iaction),time).

;axiom Init Power AssignRole
[iaction,agent1,agent2,role,nfluent,tinit,aid,time1,time]
iaction=AssignRole(agent1,agent2,role,nfluent) & agent1=IntSystem & time1=0 & agent2!=IntSystem &
nfluent=Auction(aid,Reg,tinit) & role=Participant ->
Initiates(Elapse(time1),Power(agent1,iaction),time).

;axiom Init Auction Registration phase
[aid,astate,tinit,time1,time]
astate=Reg & time1=0 ->
Initiates(Elapse(time1),Auction(aid,astate,tinit),time).

;axiom Init AuctionRoleOf1
[aid,tinit,role,nfluent,time1,time]
role=Auctioneer & nfluent=Auction(aid,Reg,tinit) & time1=0  ->
Initiates(Elapse(time1),RoleOf(role,nfluent),time).

;axiom Init AuctionRoleOf2
[aid,tinit,role,nfluent,time1,time]
role=Participant & nfluent=Auction(aid,Reg,tinit) & time1=0 ->
Initiates(Elapse(time1),RoleOf(role,nfluent),time).

;axiom Auction2
[astate,aid,tinit,time]
astate=Open & HoldsAt(Auction(aid,Reg,tinit),time) ->
Initiates(OpenAuction(aid),Auction(aid,astate,tinit),time).

;axiom Auction2
[astate,aid,tinit,time]
astate=Reg & HoldsAt(Auction(aid,Reg,tinit),time) ->
Terminates(OpenAuction(aid),Auction(aid,astate,tinit),time).

;axiom Role1
[role,nfluent,agent1,agent2,time]
HoldsAt(RoleOf(role,nfluent),time) ->
Initiates(AssignRole(agent1,agent2,role,nfluent),HasRole(agent2,role,nfluent),time).

;to do: test with time1 and time2 < time
;axiom Power OpenAuction
[agent1,agent2,agent3,agent4,iaction,time]
agent1=IntSystem &  agent2=Bob & iaction=OpenAuction(01) &
Happens(AssignRole(agent1,agent3,Participant,Auction(01,Reg,4)),time) &
Happens(AssignRole(agent1,agent4,Participant,Auction(01,Reg,4)),time) &
Happens(AssignRole(agent1,agent2,Auctioneer,Auction(01,Reg,4)),time)  ->
Happens(Empower(agent1,agent2,iaction),time).

;CreateNorm
[time1,nid,agent1,agent3,tpfluent1,tpfluent2,tpfluent3,role,nevent,nfluent,time]
 time1=0 & nid=N1 & agent1=Bob & agent3=IntSystem & role=Auctioneer &
 nfluent=Auction(01,Reg,4) & 
 tpfluent1=TPDoneOpenAuction0145Exist & tpfluent2=TPTrue & tpfluent3=TPDonePayBobAuctionHouse167Exist &
 nevent=Elapse(3) ->
 Initiates(AssignRole(agent3,agent1,role,nfluent),
 Norm(nid,agent1,agent3,tpfluent1,tpfluent2,nevent,tpfluent3),time).
 
 ;ActivateNorm
 [nid,agent1,agent2,tpfluent1,tpfluent2,tpfluent3,nevent,source,time]
 source=SNorm & HoldsAt(Norm(nid,agent1,agent2,tpfluent1,tpfluent2,nevent,tpfluent3),time) &
 Happens(nevent,time) ->
 Happens(AttCreateComm(agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
 
 ;Axiom PassiveSanction
 ;insert npower in the norm
 
 ;Axiom ActiveSanction
 [nid,agent1,agent2,tpfluent1,tpfluent2,tpfluent3,tpfluent4,nevent,tend,source,time]
 HoldsAt(Norm(nid,agent1,agent2,tpfluent1,tpfluent2,nevent,tpfluent3),time) &
 HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,SNorm,nid),time) &
 tpfluent1=TPDoneOpenAuction0145Exist & tend=5 & tpfluent4=TPTrue & source=Sanction &
 Happens(Elapse(tend),time)  ->
 Happens(AttCreateComm(agent1,agent2,tpfluent3,tpfluent4,source,nid),time).
 
 ;C04
 [state,agent1,agent2,tpfluent1,tpfluent2,source,nid,time]
  state=Fulfilled & 
  Happens(OpenAuction(01),time) & time>=4-1 & time<5 ->
  Initiates(AttCreateComm(agent1,agent2,tpfluent1,tpfluent2,source,nid),
  Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
  
  ;!HoldsAt(Comm(state2,agent1,agent2,tpfluent1,tpfluent2,source,nid),time) & 
  
  ;C03
  [state,agent1,agent2,tpfluent1,tpfluent2,source,nid,time]
  state=Pending & tpfluent1=TPDoneOpenAuction0145Exist &
  !Happens(OpenAuction(01),time) &
  HoldsAt(ETP(tpfluent1,Undef),time) & HoldsAt(ETP(tpfluent2,True),time)  ->
  Initiates(AttCreateComm(agent1,agent2,tpfluent1,tpfluent2,source,nid),
  Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
  
  ;C03
  [state,agent1,agent2,tpfluent1,tpfluent2,source,nid,time]
  state=Pending & tpfluent1=TPDonePayBobAuctionHouse167Exist &
  HoldsAt(ETP(tpfluent1,Undef),time) & HoldsAt(ETP(tpfluent2,True),time)  ->
  Initiates(AttCreateComm(agent1,agent2,tpfluent1,tpfluent2,source,nid),
  Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).

 ;!HoldsAt(Comm(state2,agent1,agent2,nfluent1,nfluent2),time) & 
  
 ;C3 Pending->Fulfilled 
 [state,aid,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
 state=Fulfilled & aid=01 &
 tpfluent1=TPDoneOpenAuction0145Exist & tend=5 & time<tend &
 HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
 Initiates(OpenAuction(aid),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
  
 ;C5 Pending -> Fulfilled 
 [state,aid,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
 state=Pending & aid=01 &
 tpfluent1=TPDoneOpenAuction0145Exist & tend=5 & time<tend &
 HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
 Terminates(OpenAuction(aid),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
 
 ;C4 Pending->Violated 
 [state,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
  state=Violated &
  tpfluent1=TPDoneOpenAuction0145Exist & tend=5 &
  HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
  Initiates(Elapse(tend),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
 
 ;C5 Pending -> Violated 
  [state,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
  state=Pending &
  tpfluent1=TPDoneOpenAuction0145Exist & tend=5 & 
  HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
  Terminates(Elapse(tend),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
  
  ;C4 Pending->Violated 
  [state,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
  state=Violated &
  tpfluent1=TPDonePayBobAuctionHouse167Exist & tend=7 &
  HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
  Initiates(Elapse(tend),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
   
  ;C5 Pending -> Violated 
  [state,agent1,agent2,tpfluent1,tpfluent2,tend,source,nid,time]
  state=Pending &
  tpfluent1=TPDonePayBobAuctionHouse167Exist & tend=7 & 
  HoldsAt(Comm(Pending,agent1,agent2,tpfluent1,tpfluent2,source,nid),time)  ->
  Terminates(Elapse(tend),Comm(state,agent1,agent2,tpfluent1,tpfluent2,source,nid),time).
  
;TP1 axiom to create temporal propositions
[tpfluent,time] 
tpfluent=TPDoneOpenAuction0145Exist &
!HoldsAt(TPDoneOpenAuction0145Exist(),time) -> 
Initiates(AttCreateTP(tpfluent),TPDoneOpenAuction0145Exist(),time).

;TP1 axiom to create temporal propositions
[tpfluent,time] 
tpfluent=TPDonePayBobAuctionHouse167Exist &
!HoldsAt(TPDonePayBobAuctionHouse167Exist(),time) -> 
Initiates(AttCreateTP(tpfluent),TPDoneOpenAuction0145Exist(),time).

;ETP0
[value,tpfluent,time]
value=Undef  -> 
Initiates(AttCreateTP(tpfluent),ETP(tpfluent,value),time).

;ETP0 special
[value,tpfluent,time1,time]
value=True  & time1=0 & tpfluent=TPTrue -> 
Initiates(Elapse(time1),ETP(tpfluent,value),time).

;ETPE3
[value,aid,tpfluent,time] 
value=True & tpfluent=TPDoneOpenAuction0145Exist &
HoldsAt(ETP(tpfluent,Undef),time) & aid=01 & time>=4-1 & time<5 -> 
Initiates(OpenAuction(aid),ETP(tpfluent,value),time).

;ETP1
[value,aid,tpfluent,time] 
value=Undef & tpfluent=TPDoneOpenAuction0145Exist &
HoldsAt(ETP(tpfluent,Undef),time) & aid=01 & 
time>=4-1 & time<5 -> 
Terminates(OpenAuction(aid),ETP(tpfluent,value),time).

;ETPE2 ETP becomes False 
[value,tpfluent,tend,time] 
value=False & tpfluent=TPDoneOpenAuction0145Exist &
HoldsAt(ETP(tpfluent,Undef),time) & tend=5 -> 
Initiates(Elapse(tend),ETP(tpfluent,value),time).

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

;ETPE2 ETP becomes False 
[value,tpfluent,tend,time] 
value=False & tpfluent=TPDonePayBobAuctionHouse167Exist &
HoldsAt(ETP(tpfluent,Undef),time) & tend=7 -> 
Initiates(Elapse(tend),ETP(tpfluent,value),time).

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

[fluent]!HoldsAt(fluent,0).
!HoldsAt(TPDoneOpenAuction0145Exist(),0).
!HoldsAt(TPDonePayBobAuctionHouse167Exist(),0).
!HoldsAt(TPTrue(),0).

;HISTORY OF THE SYSTEM
 Happens(AttCreateTP(TPDoneOpenAuction0145Exist),0).
 Happens(AttCreateTP(TPDonePayBobAuctionHouse167Exist),0).
 Happens(ExchMsgD(Declare,IntSystem,Bob,AssignRole(IntSystem,Bob,Auctioneer,Auction(01,Reg,4))),1). 
 Happens(ExchMsgD(Declare,IntSystem,Carl,AssignRole(IntSystem,Carl,Participant,Auction(01,Reg,4))),1). 
 Happens(ExchMsgD(Declare,IntSystem,Luke,AssignRole(IntSystem,Luke,Participant,Auction(01,Reg,4))),1). 
 Happens(ExchMsgD(Declare,Bob,Carl,OpenAuction(01)),4).
 
  
completion Happens

range time 0 8
range offset 1 1
range tinit 4 4
range tend 5 7

;End of file.