-- 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