/* Self-stabilizing leader election algorithm (Fischer and Jiang, OPODIS'06) in Spin 
   complete network - 4 agent version - weak fairness 
*/

/* nr of processes */
#define N	4
#define HASLEADER ((detectorcorrect == 0) -> (detector) : (leader[0] + leader[1] + leader[2] + leader[3] > 0))

bit detectorcorrect;
bool detector;
bit leader[N];

/*Rule 1*/
proctype Rule1(int i; int r) {
	doaction:
	atomic{
		if
			:: (leader[i] == 1 && leader[r] == 1) -> leader[r] = 0;
		fi;
	}
	goto doaction;
}

/*Rule 2*/
proctype Rule2(int i; int r) {
doaction:
	atomic{
		if
			:: (leader[i] == 0 && leader[r] == 0 && !HASLEADER) -> leader[i] = 1;
		fi;	
	}
	goto doaction;
}

/*Rule 3*/
proctype Rule3(int i;int r) {
doaction:
	atomic{
		if
			:: (leader[i] == 0 && leader[r] == 0 && HASLEADER) -> skip;
		fi;
	}
	goto doaction;
}


/* eventual leader detector
*/
proctype DetectorCorrect() {
do
	:: (detectorcorrect == 0) -> 
		progress: detectorcorrect = 1;
od	
}

proctype RandomDetector() {
do
	:: (detectorcorrect == 0) -> detector = false;
	:: (detectorcorrect == 0) -> detector = true;
od	
}

init {
/* randomly select intial configuration */
if
	:: atomic{ true -> leader[0] = 0;}
	:: atomic{ true -> leader[0] = 1;}
fi;

if
	:: atomic{ true -> leader[1] = 0;}
	:: atomic{ true -> leader[1] = 1;}
fi;

if
	:: atomic{ true -> leader[2] = 0;}
	:: atomic{ true -> leader[2] = 1;}
fi;

if
	:: atomic{ true -> leader[3] = 0;}
	:: atomic{ true -> leader[3] = 1;}
fi;

printf("Initial configuration has been initialized.\n");

/*Detector*/
run DetectorCorrect();
run RandomDetector();

/*Rule 1*/
run Rule1(0,1);
run Rule1(1,0);
run Rule1(0,2);
run Rule1(2,0);
run Rule1(0,3);
run Rule1(3,0);
run Rule1(1,2);
run Rule1(2,1);
run Rule1(1,3);
run Rule1(3,1);
run Rule1(2,3);
run Rule1(3,2);

/*Rule 2*/
run Rule2(0,1);
run Rule2(1,0);
run Rule2(0,2);
run Rule2(2,0);
run Rule2(0,3);
run Rule2(3,0);
run Rule2(1,2);
run Rule2(2,1);
run Rule2(1,3);
run Rule2(3,1);
run Rule2(2,3);
run Rule2(3,2);

/*Rule 3*/
run Rule3(0,1);
run Rule3(1,0);
run Rule3(0,2);
run Rule3(2,0);
run Rule3(0,3);
run Rule3(3,0);
run Rule3(1,2);
run Rule3(2,1);
run Rule3(1,3);
run Rule3(3,1);
run Rule3(2,3);
run Rule3(3,2);

}
