/* Self-stabilizing leader election algorithm (Fischer and Jiang, OPODIS'06) in Spin 
   ring network - 3 agent version - local fairness 
*/

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

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


/* Rule 1*/
proctype Rule1(int i; int r) {
	doaction:
	atomic{
		if
			:: (!HASLEADER) 
				-> bullet[i] = 1; leader[i] = 1; shield[i] = 1; printf("RULE_1(%d,%d)\n",i,r);
		fi
	}
	goto doaction;
}

/*Rule 2*/
proctype Rule2(int i; int r) {
doaction:
	atomic{
		if
			:: (leader[i] == 0 && shield[i] == 1 && HASLEADER) 
				-> leader[i] = 0; shield[i] = 0; bullet[r] = 0; shield[r] = 1; printf("RULE_2(%d,%d)\n",i,r);
		fi	
	}
	goto doaction;
}

/*Rule 3*/
proctype Rule3(int i; int r) {
doaction:
	atomic{
		if
			:: (leader[i] == 1 && shield[i] == 1 && HASLEADER) 
				-> bullet[i] = 1; leader[i] = 1; shield[i] = 0; bullet[r] = 0; shield[r] = 1; printf("RULE_3(%d,%d)\n",i,r);
		fi	
	}
	goto doaction;
}

/*Rule 4*/
proctype Rule4(int i; int r) {
doaction:
	atomic{
		if
			:: (leader[i] == 1 && shield[i] == 0 && HASLEADER && bullet[r] == 0) 
				-> bullet[i] = 1; leader[i] = 1; shield[i] = 0; bullet[r] = 0; printf("RULE_4(%d,%d)\n",i,r);
		fi	
	}
	goto doaction;
}

/*Rule 5*/
proctype Rule5(int i; int r) {
doaction:
	atomic{
		if
			:: (shield[i] == 0 && HASLEADER && bullet[r] == 1) 
				-> bullet[i] = 1; leader[i] = 0; shield[i] = 0; bullet[r] = 0; printf("RULE_5(%d,%d)\n",i,r);
		fi	
	}
	goto doaction;
}

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

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


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

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

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

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 -> shield[0] = 0;}
	:: atomic{ true -> shield[0] = 1;}
fi;

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

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

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

/*Detector*/
/*run DetectorCorrect();
run RandomDetector();*/
detectorcorrect = 1;

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

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

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

/*Rule 4*/
run Rule4(0,1);
run Rule4(1,2);
run Rule4(2,0);

/*Rule 5*/
run Rule5(0,1);
run Rule5(1,2);
run Rule5(2,0);

}
