% Module implementing a Cell process
module Cell:
input RequestIn, GrantIn, TokenIn;
output GrantOut, TokenOut, AckOut;

every immediate [GrantIn or TokenIn] do
   present RequestIn then
      emit AckOut
   else
      emit GrantOut end
end
||
every immediate TokenIn do
   await tick;
   emit TokenOut
end
.

% A dummy module to through a token in the ring at the first instant
module Init:
output Token;

emit Token
.

% The module that implements the bus arbiter with 4 cells process running
% in parallel and concurently for a bus access.
module Arbiter5:
input RequestIn1, RequestIn2, RequestIn3, RequestIn4, RequestIn5;
output AckOut1, AckOut2, AckOut3, AckOut4, AckOut5;

signal G1, G2, G3, G4, G5, T1, T2, T3, T4, T5  in
     run Init[signal T1/Token]
 ||  run Cell[signal RequestIn1/RequestIn, AckOut1/AckOut,
                     G1/GrantIn, G2/GrantOut, T1/TokenIn, T2/TokenOut]
 ||  run Cell[signal RequestIn2/RequestIn, AckOut2/AckOut,
                     G2/GrantIn, G3/GrantOut, T2/TokenIn, T3/TokenOut]
 ||  run Cell[signal RequestIn3/RequestIn, AckOut3/AckOut,
                     G3/GrantIn, G4/GrantOut, T3/TokenIn, T4/TokenOut]
 ||  run Cell[signal RequestIn4/RequestIn, AckOut4/AckOut,
                     G4/GrantIn, G5/GrantOut, T4/TokenIn, T5/TokenOut]
 ||  run Cell[signal RequestIn5/RequestIn, AckOut5/AckOut,
                     G5/GrantIn, G1/GrantOut, T5/TokenIn, T1/TokenOut]
end.