-------------------------------------------------------------------------------
-- Trivial mutual exclusion protocol 1b_p1
-- (1 variable, simple conditions, starvation-free)
-- Note: this algorithm corresponds to the first primitive solution mentioned
-- in [Peterson-81, upper part of Fig. 2]
-------------------------------------------------------------------------------

module trivial (ARCH_1B) is

!nat_bits 6 -- use 6 bits to store natural numbers

(*
 * Process P (i) competing for the access to critical section
 * where i = 0 .. N-1, j = (i+1) mod N
 *
 *   loop
 *      non critical section ;
 *      while B != i do
 *      end while ;
 *      critical section ;
 *      B := j
 *   end loop
 *)

process P [NCS:Pid, CS:Access, B:Operation] (i:Pid) is
   var j, b: Nat in
   j := (Nat (i) + 1) mod N;
   loop
      NCS (i);
      loop L in
         B (Read, ?b, i);
         if b == i then break L end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      B (Write, j, i)
   end loop
   end var
end process

-------------------------------------------------------------------------------

process Main [NCS:Pid, CS:Access, B:Operation, MU:Latency] is
   Arch_1b [NCS, CS, B, MU]
end process

end module