module phil:

%% Declarations

input	PROClb, PROCrb, PROCle, PROCre, go; 
output	READYlplus,READYrplus,eat,think;
output	READYlminus,READYrminus;

%% Instructions 

 loop
   abort 
     sustain think
   when go; 
   abort
      sustain  READYlplus;
   when PROClb;
   abort
      sustain  READYrplus;
   when PROCrb;
   emit eat; 
   await tick;
   abort
      sustain  READYlminus;
   when PROCle;
   abort
      sustain  READYrminus;
   when PROCre;
   
  end;

end module


module fork:

input 	PROClb,PROCle,PROCrb,PROCre;
output	READYlminus, READYrminus, READYlplus, READYrplus, fork_busy;

loop
   abort
     [
      sustain READYlminus;
      ||
      sustain READYrminus;
     ]
   when [PROClb or PROCrb];
   present PROClb then 
     abort
      [
       sustain READYlplus;
      ||
       sustain fork_busy;
      ]
     when PROCle;
   else
     abort
      [
       sustain READYrplus;
       ||
       sustain fork_busy;
      ]
     when PROCre;
   end;   
end

end module


module DP:

input TRIGGER1b1, TRIGGER1b2,TRIGGER1e1,TRIGGER1e2;
input TRIGGER2b1, TRIGGER2b2,TRIGGER2e1,TRIGGER2e2;

input go1,go2;

output eat1,eat2,think1,think2;

output fork1_busy,fork2_busy; 
%fork1_free, fork1_free; fork2_free, fork2_free;

signal  PROC1b1, PROC1b2,PROC1e1,PROC1e2, 
        PROC2b1, PROC2b2,PROC2e1,PROC2e2 

in

signal 	
	READY1b1plus,READY1b2plus,READY1e1plus,READY1e2plus,
	READY1b1minus,READY1b2minus,READY1e1minus,READY1e2minus,
	READY2b1plus,READY2b2plus,READY2e1plus,READY2e2plus,
	READY2b1minus,READY2b2minus,READY2e1minus,READY2e2minus

in

[
  run phil[ signal READY1b1plus/READYlplus,   READY1e1minus/READYlminus,  
                   READY1b2plus/READYrplus,  READY1e2minus/READYrminus, 
                   PROC1b1/PROClb,  PROC1e1/PROCle,PROC1b2/PROCrb, 
                   PROC1e2/PROCre, eat1/eat, go1/go, think1/think ]
   ||
  run phil[ signal READY2b1plus/READYlplus,   READY2e1minus/READYlminus,  
                   READY2b2plus/READYrplus,  READY2e2minus/READYrminus, 
                   PROC2b1/PROClb,  PROC2e1/PROCle,PROC2b2/PROCrb, 
                   PROC2e2/PROCre, eat2/eat, go2/go, think2/think ]

   ||
  run fork[ signal READY1b1minus/READYlminus, READY1e1plus/READYlplus,
                   READY2b1minus/READYrminus, READY2e1plus/READYrplus,
                   PROC1b1/PROClb,PROC1e1/PROCle,PROC2b1/PROCrb,PROC2e1/PROCre,
                   fork1_busy/fork_busy ] 
   ||
  run fork[ signal READY2b2minus/READYlminus, READY2e2plus/READYlplus,
                   READY1b2minus/READYrminus, READY1e2plus/READYrplus,
                   PROC2b2/PROClb,PROC2e2/PROCle,PROC1b2/PROCrb,PROC1e2/PROCre,
                   fork2_busy/fork_busy ]
   ||
  run Scheduler
 
]

end signal

end signal

end module


module Scheduler:

input TRIGGER1b1, TRIGGER1b2,TRIGGER1e1,TRIGGER1e2;
input TRIGGER2b1, TRIGGER2b2,TRIGGER2e1,TRIGGER2e2;

input READY1b1plus,READY1b2plus,READY1e1plus,READY1e2plus,
      READY1b1minus,READY1b2minus,READY1e1minus,READY1e2minus,
      READY2b1plus,READY2b2plus,READY2e1plus,READY2e2plus,
      READY2b1minus,READY2b2minus,READY2e1minus,READY2e2minus;

output PROC1b1, PROC1b2,PROC1e1,PROC1e2;
output PROC2b1, PROC2b2,PROC2e1,PROC2e2;

%%
%% 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 TRIGGER1b1 # TRIGGER1b2 #TRIGGER1e1 # TRIGGER1e2 # TRIGGER2b1 # 
TRIGGER2b2 # TRIGGER2e1 # TRIGGER2e2;

%%
%% Run ONE_SCHEDULER, one for each channel.
%%
signal SEL10, SEL20, SEL01, SEL02 in 
	[
	    run ONE_SCHEDULER [ signal 	READY1b1plus/READYi, 
					READY1b1minus/READYj, PROC1b1/PROC, 
					SEL10/SELi, SEL01/SELj,
					TRIGGER1b1/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY1e1plus/READYi, 
					READY1e1minus/READYj, PROC1e1/PROC, 
					SEL10/SELi, SEL01/SELj,
					TRIGGER1e1/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY1b2plus/READYi, 
					READY1b2minus/READYj, PROC1b2/PROC, 
					SEL10/SELi, SEL02/SELj,
					TRIGGER1b2/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY1e2plus/READYi, 
					READY1e2minus/READYj, PROC1e2/PROC, 
					SEL10/SELi, SEL02/SELj,
					TRIGGER1e2/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY2b1plus/READYi, 
					READY2b1minus/READYj, PROC2b1/PROC, 
					SEL20/SELi, SEL01/SELj,
					TRIGGER2b1/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY2e1plus/READYi, 
					READY2e1minus/READYj, PROC2e1/PROC, 
					SEL20/SELi, SEL01/SELj,
					TRIGGER2e1/TRIGGER ]
	||
	    run ONE_SCHEDULER [ signal 	READY2b2plus/READYi, 
					READY2b2minus/READYj, PROC2b2/PROC, 
					SEL20/SELi, SEL02/SELj,
					TRIGGER2b2/TRIGGER ]
        ||
	    run ONE_SCHEDULER [ signal 	READY2e2plus/READYi, 
					READY2e2minus/READYj, PROC2e2/PROC, 
					SEL20/SELi, SEL02/SELj,
					TRIGGER2e2/TRIGGER ]

        ]

end signal

end module


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

input 		READYi, READYj;
input 		TRIGGER;
output		PROC;
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;
		||
		    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