:- dynamic ct/3.
:- multifile ct/3.

ct(removeService(D,E), (
	downN(D),
	not(
		standbyN(S),
		D \= S,
		backupRelation(_,D,S)
	)
),(
	delete(downN(D)),
	add(emptyN(E))
)).

ct(initializeEmptyNode(E), (
	not(emptyN(E))
),(
	add(emptyN(E))
)).
%ct(initializeEmptyNode(A), (
%	not(initNode(A),emptyNode(E))
%),(
%	add(emptyNode(E)),
%	add(initNode(A))
%)).


ct(powerOnService(E,A), ( 
	emptyN(E)
),(
	add(upN(A)),
	delete(emptyN(E))
)).

%open_world_cts([
%	powerOnService,removeService,initializeEmptyNode
%]).

ct(registerService(S,A), (
    upN(S)
),(
    delete(upN(S)),
    add(activeN(A))
)).

ct(unregisterService(S,U), (
    activeN(S),
    not(
    	initN(S2),
    	S2 \= S,
    	backupRelation(_b,S,S2)
    )
),(
	delete(activeN(S)),
	add(upN(U))
)).

ct(standbyService(A,U,Rb,S), (
	activeN(A),
	upN(U),
	A \= U,
	not( backupRelation(Rb,A,U) )

),(
	delete(upN(U)),
	add(standbyN(S)),
	add(backupRelation(Rb,A,S))
)).

ct(detachService(A,S,Rb,U), (
	activeN(A),
	standbyN(S),
	A \= S,
	backupRelation(Rb,A,S)
),(
	delete(backupRelation(Rb,A,S)),
	delete(standbyN(S)),
	add(upN(U))
)).

ct(failoverService(D,S,Rb,A), (
	downN(D),
	standbyN(S),
	D \= S,
	backupRelation(Rb,D,S)
),(
	delete(backupRelation(Rb,D,S)),
	delete(standbyN(S)),
	add(activeN(A))
)).