/* Jon Rafkind
 * Dijkstra's algorithm for discovering a sequence of passive nodes.
 *
 * node0 initially sends the white token to node1.
 * For a given node, N, if it is in a passive state it waits for either the token
 * to come by or for it to be assigned work. If the token comes by it immediately
 * sends the token back out, black if N sent work, otherwise the color of the token
 * if N hasn't sent work.
 * If N is active then it either assigns more work or immediately becomes passive and receives
 * the token.
 */

#define N 2
#define WORK 1

mtype = { BlackToken, WhiteToken, NoneToken,
	  WhiteN, BlackN,
	  ActiveN, PassiveN };

chan workqArray[ N ] = [0] of { bit };
chan tokqArray[ N ] = [1] of { mtype };
mtype nodestate[ N ];

bit terminated = 0;

inline sendWork( num, id ){
	do
		:: num > 0 -> num--
		:: num < N - 1 -> num++
		:: num != id -> goto Done
	od;
	Done:
		skip;
}

proctype node( chan tokIn, tokOut, workIn; byte myid ){
	mtype nodecolor = WhiteN;
	mtype localtoken = NoneToken;

	/* nodes can write to itself */
	/*
	xr tokIn;
	xs tokOut;
	*/

	byte sentwork = 0;
	byte kind;

	/* assume node 0 hasn't assigned work already */
	if
	:: myid == 0 ->
		tokOut!WhiteToken
	:: else -> skip
	fi;


	/* dont feel like waiting for ourselves to become passive
	 * so if a node receives the token just become passive
	 */

	do
	:: terminated -> break
	:: (nodestate[ myid ] == PassiveN) ->
		printf( "%d is passive\n", myid );
		if
		:: workIn?WORK ->
			printf( "%d has work\n", myid );
			nodestate[ myid ] = ActiveN
		:: tokIn?WhiteToken ->
			if
			:: sentwork == 1 ->
				printf( "%d sent black token\n", myid );
				tokOut!BlackToken;
				sentwork = 0
			:: sentwork == 0 ->
				if
				:: myid == 0 ->
					printf( "Node 0 saw a white token\n" );
					terminated = 1
				:: else ->
					printf( "%d sent white token\n", myid );
					tokOut!WhiteToken
				fi
			fi
		:: tokIn?BlackToken ->
			printf( "%d received black token\n", myid );
			if
			:: myid == 0 ->
				printf( "%d sent white token\n", myid );
				tokOut!WhiteToken
			:: else ->
				printf( "%d sent black token\n", myid );
				tokOut!BlackToken
			fi
		// :: timeout -> skip
		// :: else -> skip
		fi
	:: nodestate[ myid ] == ActiveN ->
		printf( "%d is active\n", myid );
		if
		:: true ->
			nodestate[ myid ] = PassiveN
		:: workIn?WORK ->
			skip
		:: true ->
			byte pick = 0;
			sendWork( pick, myid );
			atomic{
				printf( "%d active send work to %d\n", myid, pick );
				workqArray[ pick ]!WORK;
				printf( "%d sent work to %d\n", myid, pick );
			}
			sentwork = 1;
		:: tokIn?kind ->
			printf( "%d active received token %d. white = %d. black = %d\n", myid, kind, WhiteToken, BlackToken );
			nodestate[ myid ] = PassiveN;
			tokIn!kind
			/*
		:: timeout ->
			// asked for work but didnt get it
			skip
			*/
		fi
	od;

	end: skip
}

init{
	byte i = 0;
	atomic{
		do
		:: i < N ->
			nodestate[ i ] = ActiveN;
			run node( tokqArray[ i ], tokqArray[(i+1) % N], workqArray[ i ], i );
			i++
		:: i == N ->
			break
		od
	}

	/* stop the simulation after some steps steps */
	/*
	byte steps = 0;
	do
		:: steps <= N * 50 -> steps++
		:: steps > N * 50 -> 
			printf( "terminate!\n" );
			terminated = 1;
			break
	od
	*/
}

never{
	skip
}