The DisCo Home Page

Exchange of Values

This specification describes how processes may exchange the values of their x attributes. The || separator denotes parallel assignment.

The next layer superimposes termination detection on this layer.

system PROCESSES is

 	class PROCESS is
		X: integer;
		NEXT: PROCESS;
 	end PROCESS;

        action EXCHANGE by A:PROCESS; B:PROCESS is
        when A.NEXT = B and A.X > B.X do
		A.X := B.X || B.X := A.X; 
        end EXCHANGE;

end PROCESSES;

Give feedback.