--Description of FIFO queue chip designed by F. Baskett
--Specification by R.Burstall and N.Suzuki

guardian	Init^ onlywhen ~ReadRequest & ~WriteRequest,
			ReadRequest^ onlywhen DataAv,
			WriteRequest^ onlywhen SpaceAv;

dataflow	DataAv <= delay(~ReadRequest) & rp<wp,
			SpaceAv <= delay(~WriteRequest) & wp<wp+size,
			A[wp] <= DataIn,
			DataOut <= A[rp];

control		repeat {
				when Init^ _ rp := wp := 0;
				
					on Init^ _ exit in
				par [ repeat {
							when ReadRequest^ _ skip;
							when ReadRequest^ _ rp := rp+1}
						//
						repeat {
							when WriteRequest^ _ skip;
							when WriteRequest^ _ wp := wp+1}
				]
			}
(635)\100u8U7u8U14f3 1f0 32u8U26u8U11u8U31f3 1f0 43f3 1f0 55u7U2u6U7u4U5f3 1f0 1f3 1f0 26u2U7f3 1f0 1u4U1u2U5u3U3u6U10u4U14f3 1f0 1u4U9u4U12f3 1f0 1f3 1f0 28u6U10u4U15f3 1f0 1u4U9u4U13f3 1f0 1f3 1f0