-- 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 ← TRUE; DataAv ← FALSE;
            PAR { 
                DO 
                    WHEN ReadRequest UP : {
                        DataAv←FALSE; rp←rp+1;
                        DOut←A[rp]; SpaceAv ← ~WriteRequest AND wp<rp+size};
                    WHEN ReadRequest DOWN: DataAv←rp<wp;
                    ENDLOOP
                        //
                DO 
                    WHEN WriteRequest UP : {
                        SpaceAv←FALSE; wp←wp+1; A[wp]←DIn;
                        DOut←A[rp]; DataAv←~ReadRequest AND rp<wp};
                    WHEN WriteRequest DOWN: SpaceAv←wp<rp+size;
                    ENDLOOP
            }
        ENDLOOP
    };
     
NULL

}. -- end of FIFO DEFINITION