/* Self-stabilizing Token-Circulation in a Directed Ring (Angluin, Aspnes, Fischer and Jiang, OPODIS 2005) in Spin 
   4 agent version - from any configuration to safe configuration by sequential selector.
*/

/* nr of processes */
#define N	5

bit leader[N];
bit token[N];
bit label[N];
int turn;

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

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

/*watchDog*/
proctype watchdog()
{
	do
	:: timeout -> 
		if
			:: turn <= (N-2) -> turn=turn+1;
		fi;	
	od
}


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

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

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

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

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

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

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

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

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

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

}


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

run watchdog();

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

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

}
