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

guardianInit↑ onlywhen ~ReadRequest & ~WriteRequest,
ReadRequest↑ onlywhen DataAv,
WriteRequest↑ onlywhen SpaceAv;

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

controlrepeat {
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}
]
}