module Main:
input RequestIn1,RequestIn2,RequestIn3,RequestIn4,RequestIn5;
output AckOut1,AckOut2,AckOut3,AckOut4,AckOut5,
    DCERR1, DCERR2, DCERR3;

signal RequestIn,AckOut,Lostcycle in
run Arbiter5
||
    run proparbobs1mod[signal DCERR1/DCERR]
||
    run proparbobs2mod[signal DCERR2/DCERR]
||
    run proparbobs3mod[signal DCERR3/DCERR]
||
    every immediate [(RequestIn1)]
    do emit RequestIn end
||
    every immediate [(AckOut1)]
    do emit AckOut end
||
    every immediate [((((((RequestIn1) or (RequestIn2)) or (RequestIn3)) or (RequestIn4)) or (RequestIn5)) and not (((((AckOut1) or (AckOut2)) or (AckOut3)) or (AckOut4)) or (AckOut5)))]
    do emit Lostcycle end
end
end module
% 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.
module proparbobs1mod:
input RequestIn, AckOut, Lostcycle ;
output DCERR ;

signal St1, St2 in
emit St1 ;
loop
 present
 case St1 do 
   present
     case [St1 and not RequestIn and not AckOut] do 
            await tick; emit St1 
     case [St1 and not RequestIn and AckOut] do 
           emit DCERR;
            await tick; emit St2 
     case [St1 and RequestIn] do 
            await tick; emit St1 
     else await tick
   end present
 case St2 do 
   present
     case [St2] do 
           emit DCERR;
            await tick; emit St2 
     else await tick
   end present
 else await tick
 end present
end loop
end signal
end module
module proparbobs2mod:
input RequestIn, AckOut, Lostcycle ;
output DCERR ;

signal St1, St2 in
emit St1 ;
loop
 present
 case St1 do 
   present
     case [St1 and not Lostcycle] do 
            await tick; emit St1 
     case [St1 and Lostcycle] do 
           emit DCERR;
            await tick; emit St2 
     else await tick
   end present
 case St2 do 
   present
     case [St2] do 
           emit DCERR;
            await tick; emit St2 
     else await tick
   end present
 else await tick
 end present
end loop
end signal
end module
module proparbobs3mod:
input RequestIn, AckOut, Lostcycle ;
output DCERR ;

signal St1, St2, St3, St4, St5, St6 in
emit St1 ;
loop
 present
 case St1 do 
   present
     case [St1 and not RequestIn] do 
            await tick; emit St1 
     case [St1 and RequestIn and not AckOut] do 
            await tick; emit St2 
     case [St1 and RequestIn and AckOut] do 
            await tick; emit St1 
     else await tick
   end present
 case St2 do 
   present
     case [St2 and not RequestIn] do 
            await tick; emit St1 
     case [St2 and RequestIn and not AckOut] do 
            await tick; emit St3 
     case [St2 and RequestIn and AckOut] do 
            await tick; emit St1 
     else await tick
   end present
 case St3 do 
   present
     case [St3 and not RequestIn] do 
            await tick; emit St1 
     case [St3 and RequestIn and not AckOut] do 
            await tick; emit St4 
     case [St3 and RequestIn and AckOut] do 
            await tick; emit St1 
     else await tick
   end present
 case St4 do 
   present
     case [St4 and not RequestIn] do 
            await tick; emit St1 
     case [St4 and RequestIn and not AckOut] do 
            await tick; emit St5 
     case [St4 and RequestIn and AckOut] do 
            await tick; emit St1 
     else await tick
   end present
 case St5 do 
   present
     case [St5 and not RequestIn] do 
            await tick; emit St1 
     case [St5 and RequestIn and not AckOut] do 
           emit DCERR;
            await tick; emit St6 
     case [St5 and RequestIn and AckOut] do 
            await tick; emit St1 
     else await tick
   end present
 case St6 do 
   present
     case [St6] do 
           emit DCERR;
            await tick; emit St6 
     else await tick
   end present
 else await tick
 end present
end loop
end signal
end module