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

/* nr of processes */
#define N	7
#define HASLEADER ((detectorcorrect == 0) -> (detector) : (leader[0] + leader[1] + leader[2] + leader[3] + leader[4] + leader[5]+ leader[6]> 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;

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

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

if
	:: atomic{ true -> leader[6] = 0;}
	:: atomic{ true -> leader[6] = 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(0,4);
run Rule1(4,0);
run Rule1(0,5);
run Rule1(5,0);
run Rule1(0,6);
run Rule1(6,0);
run Rule1(1,2);
run Rule1(2,1);
run Rule1(1,3);
run Rule1(3,1);
run Rule1(1,4);
run Rule1(4,1);
run Rule1(1,5);
run Rule1(5,1);
run Rule1(1,6);
run Rule1(6,1);
run Rule1(2,3);
run Rule1(3,2);
run Rule1(2,4);
run Rule1(4,2);
run Rule1(2,5);
run Rule1(5,2);
run Rule1(2,6);
run Rule1(6,2);
run Rule1(3,4);
run Rule1(4,3);
run Rule1(3,5);
run Rule1(5,3);
run Rule1(3,6);
run Rule1(6,3);
run Rule1(4,5);
run Rule1(5,4);
run Rule1(4,6);
run Rule1(6,4);
run Rule1(5,6);
run Rule1(6,5);
/*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(0,4);
run Rule2(4,0);
run Rule2(0,5);
run Rule2(5,0);
run Rule2(0,6);
run Rule2(6,0);
run Rule2(1,2);
run Rule2(2,1);
run Rule2(1,3);
run Rule2(3,1);
run Rule2(1,4);
run Rule2(4,1);
run Rule2(1,5);
run Rule2(5,1);
run Rule2(1,6);
run Rule2(6,1);
run Rule2(2,3);
run Rule2(3,2);
run Rule2(2,4);
run Rule2(4,2);
run Rule2(2,5);
run Rule2(5,2);
run Rule2(2,6);
run Rule2(6,2);
run Rule2(3,4);
run Rule2(4,3);
run Rule2(3,5);
run Rule2(5,3);
run Rule2(3,6);
run Rule2(6,3);
run Rule2(4,5);
run Rule2(5,4);
run Rule2(4,6);
run Rule2(6,4);
run Rule2(5,6);
run Rule2(6,5);
/*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(0,4);
run Rule3(4,0);
run Rule3(0,5);
run Rule3(5,0);
run Rule3(0,6);
run Rule3(6,0);
run Rule3(1,2);
run Rule3(2,1);
run Rule3(1,3);
run Rule3(3,1);
run Rule3(1,4);
run Rule3(4,1);
run Rule3(1,5);
run Rule3(5,1);
run Rule3(1,6);
run Rule3(6,1);
run Rule3(2,3);
run Rule3(3,2);
run Rule3(2,4);
run Rule3(4,2);
run Rule3(2,5);
run Rule3(5,2);
run Rule3(2,6);
run Rule3(6,2);
run Rule3(3,4);
run Rule3(4,3);
run Rule3(3,5);
run Rule3(5,3);
run Rule3(3,6);
run Rule3(6,3);
run Rule3(4,5);
run Rule3(5,4);
run Rule3(4,6);
run Rule3(6,4);
run Rule3(5,6);
run Rule3(6,5);
}
