module Scheduler:

input	READY_CH1plus(integer),  READY_CH2plus(integer),  
	READY_CH1minus, READY_CH2minus;

input 	TRIGGER_CH1,    TRIGGER_CH2;

output	PROC_CH1(integer),  PROC_CH2(integer); 
%%
%% The exclusion relations for processes involved in sending/receiving with
%% each other such that one process is involved in one transaction at a time.
%%
relation 	TRIGGER_CH1 # TRIGGER_CH2;

%%
%% Run ONE_SCHEDULER, one for each channel.
%%
signal SEL1, SEL2, SEL3 in 
	[
	    run ONE_SCHEDULER [ signal 	READY_CH1plus/READYi, 
					READY_CH1minus/READYj, PROC_CH1/PROC, 
					SEL1/SELi, SEL2/SELj,
					TRIGGER_CH1/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY_CH2plus/READYi, 
					READY_CH2minus/READYj, PROC_CH2/PROC,
					SEL2/SELi, SEL3/SELj,
					TRIGGER_CH2/TRIGGER ]
	]
end signal

end module


%%
%% The scheduler for one channel between process i (sender) and 
%% process j (receiver).
%%
module ONE_SCHEDULER:

input 		READYi(integer), READYj;
input 		TRIGGER;
output		PROC(integer);
inputoutput	SELi, SELj;

signal LREADYi, LREADYj in 
	loop
	    trap T in 
		    [
		    	await immediate LREADYi;
		    ||
		       	await immediate LREADYj;
		    ];
		    await tick;
		    await immediate TRIGGER;
		    emit SELi;
		    emit SELj;
		    emit PROC(?READYi);
		||
		    await 
			case SELi do 
				exit T;
			case SELj do 
				exit T;
		    end await;
	    end trap
	end loop

	||
		
	loop
	    do 
		await immediate READYi;
		sustain LREADYi
	    watching SELi
	end loop
	 
	||

	loop
	    do 
		await immediate READYj;
		sustain LREADYj
	    watching SELj
	end loop

end signal	 

end module