:- sorts
	Role;
	Slot;
	Message;
	State;
	Commitment;
	Condition.

:- variables
	msg1 :: Message;
	p,q :: Condition;
	c1 :: Commitment;
	db1,cr1,db2,cr2 :: Role.

:- objects
	NIL,BASE,CONDITIONAL,FULFILLED,BASE_DELEGATED, 
	CONDITIONAL_DELEGATED,BASE_ASSIGNED,CONDITIONAL_ASSIGNED, 
	BASE_ASSIGNED_DELEGATED,CONDITIONAL_ASSIGNED_DELEGATED,RELEASED,CANCELLED :: State;
	T :: Condition;
	cc(Role,Role,Condition,Condition) :: Commitment.
	

:- constants
	fl(Message) :: inertialFluent;

	act(Message) :: exogenousAction;

	cond(Condition) :: action;
	
	comm(Commitment) :: inertialFluent(State);

	create(Commitment),
	discharge(Commitment),
	toBase(Commitment) :: action;

	delegateTo(Role,Commitment),
	assignTo(Role,Commitment),
	cancel(Commitment),
	release(Commitment) :: action;

	active(Commitment) :: sdFluent;
	initial :: sdFluent.



caused initial if initial.

caused -initial if comm(c1)\=NIL.
caused -initial if fl(msg1).

act(msg1) causes fl(msg1).

-cond(p) causes -cond(p).

caused -active(c1) if -active(c1).

caused active(c1) if comm(c1)\=NIL & comm(c1)\=FULFILLED
	& comm(c1)\=RELEASED & comm(c1)\=CANCELLED.


%%%%%% laws about causation of the automatic commitment operations (the three rules in our papers)
caused discharge(cc(db1,cr1,p,q)) if cond(q) &
(active(cc(db1,cr1,p,q)) ++ create(cc(db1,cr1,p,q))) where db1<>cr1.

caused toBase(cc(db1,cr1,p,q)) if cond(p) &
(active(cc(db1,cr1,p,q)) ++ create(cc(db1,cr1,p,q))) where db1<>cr1 & p<>T.

%%%%%% create %%%%%%
caused comm(cc(db1,cr1,T,q))=BASE if true after
	create(cc(db1,cr1,T,q)) & 
	-(discharge(cc(db1,cr1,T,q)) ++ 
	release(cc(db1,cr1,T,q)) ++
	cancel(cc(db1,cr1,T,q)) ++
	delegateTo(db2,cc(db1,cr1,T,q)) ++
	assignTo(cr2,cc(db1,cr1,T,q))) &
	comm(cc(db1,cr1,T,q))=NIL where db1<>cr1 & q<>T.

caused comm(c1)=CONDITIONAL if true after
	create(c1) & -(discharge(c1) ++ release(c1) ++
	cancel(c1) ++ delegateTo(db2,c1) ++ assignTo(cr2,c1)) &
	comm(c1)=NIL.

%%%%%% discharge %%%%%%
caused comm(c1)=FULFILLED if true after discharge(c1).

%%%%%% release %%%%%%
caused comm(c1)=RELEASED if true after
	release(c1) & -discharge(c1) &
	(active(c1) ++ create(c1)).

%%%%%% cancel %%%%%%
caused comm(c1)=CANCELLED if true after
	cancel(c1) & -(discharge(c1) ++ release(c1)) &
	(active(c1) ++ create(c1)).

%%%%%% toBase %%%%%%
caused comm(c1)=BASE if true after
	toBase(c1) & -(discharge(c1) ++ release(c1) ++
	cancel(c1) ++ delegateTo(db2,c1) ++ assignTo(cr2,c1)) &
	comm(c1)=CONDITIONAL.

caused comm(c1)=BASE_DELEGATED if true after
	toBase(c1) & -(discharge(c1) ++ release(c1) ++
	cancel(c1) ++ delegateTo(db2,c1) ++ assignTo(cr2,c1)) &
	comm(c1)=CONDITIONAL_DELEGATED.

caused comm(c1)=BASE_ASSIGNED if true after
	toBase(c1) & -(discharge(c1) ++ release(c1) ++
	cancel(c1) ++ delegateTo(db2,c1) ++ assignTo(cr2,c1)) &
	comm(c1)=CONDITIONAL_ASSIGNED.

caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	toBase(c1) & -(discharge(c1) ++ release(c1) ++
	cancel(c1) ++ delegateTo(db2,c1) ++ assignTo(cr2,c1)) &
	comm(c1)=CONDITIONAL_ASSIGNED_DELEGATED.

%%%%%% delegate BASE --> BASE_DELEGATED %%%%%%
caused comm(c1)=BASE_DELEGATED if true after
	delegateTo(db2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=BASE.

%%%%%% delegate BASE_ASSIGNED --> BASE_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	delegateTo(db2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=BASE_ASSIGNED.

%%%%%% delegate CONDITIONAL --> CONDITIONAL_DELEGATED %%%%%%
caused comm(c1)=CONDITIONAL_DELEGATED if true after
	delegateTo(db2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1) ++ toBase(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.

%%%%%% delegate CONDITIONAL_ASSIGNED --> CONDITIONAL_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=CONDITIONAL_ASSIGNED_DELEGATED if true after
	delegateTo(db2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1) ++ toBase(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL_ASSIGNED.

%%%%%% toBase & delegate CONDITIONAL --> BASE_DELEGATED %%%%%%
caused comm(c1)=BASE_DELEGATED if true after
	delegateTo(db2,c1) & toBase(c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.

%%%%%% toBase & delegate CONDITIONAL_ASSIGNED --> BASE_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	delegateTo(db2,c1) & toBase(c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ assignTo(cr2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL_ASSIGNED.


%%%%%% delegate create all%%%%%%
caused create(cc(db2,cr1,p,q)) if
	delegateTo(db2,cc(db1,cr1,p,q)) &
	-(discharge(cc(db1,cr1,p,q)) ++
	release(cc(db1,cr1,p,q)) ++
	cancel(cc(db1,cr1,p,q)) ++
	assignTo(cr2,cc(db1,cr1,p,q))) &
	(active(cc(db1,cr1,p,q)) ++ create(cc(db1,cr1,p,q))) &
	(comm(cc(db1,cr1,p,q))=BASE ++ comm(cc(db1,cr1,p,q))=CONDITIONAL ++ 
	comm(cc(db1,cr1,p,q))=BASE_ASSIGNED ++ comm(cc(db1,cr1,p,q))=CONDITIONAL_ASSIGNED).

%%%%%% delegate & assign BASE --> BASE_ASSIGNED_DELEGATED%%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	delegateTo(db2,c1) & assignTo(cr2,c1) & 
	-(discharge(c1) ++ release(c1) ++ cancel(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=BASE.

%%%%%% delegate & assign CONDITIONAL --> CONDITIONAL_ASSIGNED_DELEGATED%%%%%%
caused comm(c1)=CONDITIONAL_ASSIGNED_DELEGATED if true after
	delegateTo(db2,c1) & assignTo(cr2,c1) & 
	-(discharge(c1) ++ release(c1) ++ cancel(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.

%%%%%% delegate & assign create all%%%%%%
caused create(cc(db2,cr2,p,q)) if
	delegateTo(db2,cc(db1,cr1,p,q)) &
	assignTo(cr2,cc(db1,cr1,p,q)) &
	-(discharge(cc(db1,cr1,p,q)) ++
	release(cc(db1,cr1,p,q)) ++
	cancel(cc(db1,cr1,p,q))) &
	(active(cc(db1,cr1,p,q)) ++ create(cc(db1,cr1,p,q))) &
	(comm(cc(db1,cr1,p,q))=BASE ++ comm(cc(db1,cr1,p,q))=CONDITIONAL).

%%%%%% assign BASE --> BASE_ASSIGNED %%%%%%
caused comm(c1)=BASE_ASSIGNED if true after
	assignTo(cr2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=BASE.

%%%%%% assign BASE_DELEGATED --> BASE_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	assignTo(cr2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=BASE_DELEGATED.

%%%%%% assign CONDITIONAL --> CONDITIONAL_ASSIGNED %%%%%%
caused comm(c1)=CONDITIONAL_ASSIGNED if true after
	assignTo(cr2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1) ++ toBase(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.

%%%%%% assign CONDITIONAL_DELEGATED --> CONDITIONAL_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=CONDITIONAL_ASSIGNED_DELEGATED if true after
	assignTo(cr2,c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1) ++ toBase(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL_DELEGATED.

%%%%%% toBase & assign CONDITIONAL --> BASE_ASSIGNED %%%%%%
caused comm(c1)=BASE_ASSIGNED if true after
	assignTo(cr2,c1) & toBase(c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.

%%%%%% toBase & assign CONDITIONAL_DELEGATED --> BASE_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	assignTo(cr2,c1) & toBase(c1) & -(discharge(c1) ++
	release(c1) ++ cancel(c1) ++ delegateTo(db2,c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL_DELEGATED.


%%%%%% assign create all%%%%%%
caused create(cc(db2,cr1,p,q)) if
	assignTo(cr2,cc(db1,cr1,p,q)) &
	-(discharge(cc(db1,cr1,p,q)) ++
	release(cc(db1,cr1,p,q)) ++
	cancel(cc(db1,cr1,p,q)) ++
	delegateTo(db2,cc(db1,cr1,p,q))) &
	(active(cc(db1,cr1,p,q)) ++ create(cc(db1,cr1,p,q))) &
	(comm(cc(db1,cr1,p,q))=BASE ++ comm(cc(db1,cr1,p,q))=CONDITIONAL ++ 
	comm(cc(db1,cr1,p,q))=BASE_DELEGATED ++ comm(cc(db1,cr1,p,q))=CONDITIONAL_DELEGATED).

%%%%%% toBase & assign & delegate CONDITIONAL --> BASE_ASSIGNED_DELEGATED %%%%%%
caused comm(c1)=BASE_ASSIGNED_DELEGATED if true after
	assignTo(cr2,c1) & toBase(c1) & delegateTo(db2,c1) & 
        -(discharge(c1) ++ release(c1) ++ cancel(c1)) &
	(active(c1) ++ create(c1)) & comm(c1)=CONDITIONAL.


%%%%%% By default all commitment operations are disabled
-create(c1) causes -create(c1).
-discharge(c1) causes -discharge(c1).
-toBase(c1) causes -toBase(c1).
-delegateTo(db2,c1) causes -delegateTo(db2,c1).
-assignTo(cr2,c1) causes -assignTo(cr2,c1).
-cancel(c1) causes -cancel(c1).
-release(c1) causes -release(c1).


:- show
act(msg1);
fl(msg1);
comm(c1)=CONDITIONAL;
comm(c1)=BASE;
initial;
active(c1).