-- FIFOImpl.sak
-- last edited by Suzuki: 20-Nov-81 16:02:15

DIRECTORY
  Connector,
  FIFO,
  Process;
  
FIFOImpl: MONITOR IMPORTS Connector, Process
  EXPORTS FIFO ={
	
FIFOFunc: PUBLIC DEVICE [size: CARDINAL] = {
	IN Init, WriteRequest, ReadRequest: BOOLEAN,
		DIn: CARDINAL
	OUT SpaceAv, DataAv: BOOLEAN, DOut: CARDINAL
	GUARDIAN {
		Initialized: BOOLEAN ← FALSE;
		DO CHOICE {
		  WHEN Init UP -> {IF ReadRequest OR WriteRequest THEN ERROR;
		   Initialized ← TRUE} ||
		  WHEN ReadRequest UP -> IF ~Initialized OR Init OR ~DataAv
		   THEN ERROR ||
		  WHEN WriteRequest UP -> IF ~Initialized OR Init OR ~SpaceAv
		   THEN ERROR}
		ENDLOOP }
	STATE A: ARRAY [1..37] OF CARDINAL, rp, wp: CARDINAL
	CONTROL
		DO 
			WHEN Init UP : rp ← wp ← 0;
			A[rp] ← DIn; DOut ← A[wp];
			SpaceAv ← FALSE; DataAv ← FALSE;
			PAR { 
				DO 
					WHEN ReadRequest UP : {
						DataAv ← FALSE; rp ← rp+1; A[rp]←DIn;
						DOut←A[wp]; SpaceAv←~WriteRequest AND wp<rp+size};
					WHEN ReadRequest DOWN: DataAv ← rp<wp
					ENDLOOP
						//
				DO 
					WHEN WriteRequest UP : {
						SpaceAv←FALSE; wp←wp+1;
						DOut←A[wp]; DataAv←~ReadRequest AND rp<wp};
					WHEN WriteRequest DOWN: SpaceAv←wp<rp+size;
					ENDLOOP
			}
		ENDLOOP
	};
	 
NULL

}. -- end of FIFO DEFINITION