/* Distributed Termination Detection - Dijkstra/Safra */

mtype = { Query, Quit, Work };

chan q[2] = [32] of { mtype, byte };

active [2] proctype N()
{	bool query_in_progress = false;
	byte s, r, n;

	assert(_pid == 0 || _pid == 1);

	q[1 - _pid]!Work,0; s++;	/* seed some work items */

accept:
	do
	:: q[_pid]?Work,0 -> r++;
		if
		:: (s < 16) -> q[1 - _pid]!Work,0; s++
		:: true
		fi

	:: empty(q[0]) && !query_in_progress && _pid == 0 ->	/* only node 0 can initiate termination */
		query_in_progress = true;			/* remember that we sent the Query msg   */
		q[1]!Query,s

	:: q[_pid]?Quit,0 ->			/* only node 1 receives this */
		assert(_pid == 1);
		break				/* 1 can now terminate */

	:: q[_pid]?Query,n ->
		if
		:: _pid == 1 ->
			q[0]!Query,r		/* respond to termination query from 0 */

		:: _pid == 0 ->			/* process response to our termination query */
			if
			:: n == s -> q[1]!Quit,0; break	/* accepted; node 0 terminates */
			:: else -> query_in_progress = false		/* rejected; try again */
			fi
		fi
	od;

	assert(empty(q[_pid]))
}