The DisCo Home Page

Termination Detection

This layer describes how processes decide when the values have been sorted. When the sorted attribute becomes true, a process knows that it holds the correct value.

system PROCESSES_COMMUNICATION import PROCESSES; is

	extend PROCESS by
		PREV: PROCESS;
		SORTED : boolean;	
	end PROCESS;

	refined EXCHANGE is
	when ... do
		...
		if A.PREV /= NULL then
			A.SORTED := FALSE;
		end if;
	end EXCHANGE;
	
	action COMMUNICATE by A:PROCESS; B:PROCESS is
	when A.NEXT = B and A.SORTED and not B.SORTED and A.X <= B.X do
		B.SORTED := TRUE;
	end COMMUNICATE;

end PROCESSES_COMMUNICATION;

Give feedback.