-------------------------------------------------------------------------------
-- Dijkstra's mutual exclusion protocol [Dijkstra-65]
-- (2 arrays + 1 variable, simple conditions, not starvation-free)
-------------------------------------------------------------------------------

module dijkstra (ARCH_5B) 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
 *
 *   loop
 *      non critical section ;
 *      A[i] := 1 ;
 *      loop L1 in
 *         if B != i then
 *            C[i] := 0 ;
 *            if A[B] == 0 then
 *               B := i
 *            end if
 *         else
 *            C[i] := 1 ;
 *            j := 0 ;
 *            loop L2
 *               if (j != i) and (C[j] == 1) then break L2 end if ;
 *               if j == N-1 then break L1 end if ;
 *               j := j + 1
 *            end loop
 *         end if
 *      end loop ;
 *      critical section ;
 *      C[i] := 0 ;
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, B, C:Operation] (i: Pid) is
   var j: Pid, b, a_b, c_j: Nat in
   loop
      NCS (i);
      A (Write, i, 1 of Nat, i);
      loop L1 in
         B (Read, ?b, i);
         if b != i then
            C (Write, i, 0 of Nat, i);
            B (Read, ?b, i);
            A (Read, b of Pid, ?a_b, i);
            if a_b == 0 then
               B (Write, Nat (i), i)
            end if
         else
            C (Write, i, 1 of Nat, i);
            j := 0 of Pid;
            loop L2 in
	       if j != i then
                  C (Read, j, ?c_j, i);
                  if c_j == 1 then break L2 end if
               end if;
               if j == (N - 1) then break L1 end if;
               j := j + 1       
            end loop
         end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      C (Write, i, 0 of Nat, i);
      A (Write, i, 0 of Nat, i)
   end loop
   end var
end process

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

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

end module