-------------------------------------------------------------------------------
-- Szymanski's basic algorithm for mutual exclusion
-- (two shared variables with five different values)
-------------------------------------------------------------------------------

module szymanski (ARCH_2B) 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
 *
 *   A[i] := 0;
 *   loop
 *      non critical section ;
 *      A[i] := 1;
 *      wait until (forall j) A[j] < 3 ;
 *      A[i] := 3;
 *      if (exists j) A[j] == 1 then
 *         A[i] := 2 ;
 *         wait until (exists j) A[j] = 4
 *      end if ;
 *      A[i] := 4 ;
 *      wait until (forall j < i) A[j] < 2 ;
 *      critical section ;
 *      wait until (forall j > i) A[j] in { 0, 1, 4 }
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A:Operation] (i: Pid) is
   var j, a_j: Nat in
   loop
      NCS (i);
      A (Write, i, 1 of Nat, i);
      j := 0;
      loop L1 in
         if (j != i) then
            loop L2 in
               A (Read, j of Pid, ?a_j, i);
               if a_j < 3 then break L2 end if
            end loop
         end if;
         if j == (N - 1) then break L1 end if;
         j := j + 1
      end loop;
      A (Write, i, 3 of Nat, i);
      j := 0;
      loop L3 in
         if (j != i) then
            A (Read, j of Pid, ?a_j, i);
            if a_j == 1 then
               A (Write, i, 2 of Nat, i);
               loop L4 in
                  j := 0;
                  loop L5 in
                     if (j != i) then
                        A (Read, j of Pid, ?a_j, i);
                        if a_j == 4 then break L3 end if
                     end if;
                     if j == (N - 1) then break L5 end if;
                     j := j + 1
                  end loop
               end loop
            end if
         end if;
         if j == (N - 1) then break L3 end if;
         j := j + 1
      end loop;
      A (Write, i, 4 of Nat, i);
      j := 0;
      loop L6 in
         if j == i then break L6 end if;
         loop L7 in
            A (Read, j of Pid, ?a_j, i);
            if a_j < 2 then break L7 end if
         end loop;
         j := j + 1
      end loop;
      CS (Enter, i); CS (Leave, i);
      j := Nat (i) + 1;
      loop L8 in
         if j == N then break L8 end if;
         loop L9 in
            A (Read, j of Pid, ?a_j, i);
            if (a_j == 0) or (a_j == 1) or (a_j == 4) then break L9 end if
         end loop;
         j := j + 1
      end loop;
      A (Write, i, 0 of Nat, i)
   end loop
   end var
end process

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

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

end module