A simple parameterized mutual exclusion algorithm

local N: int where N > 0
local x, y: int where x = 1 /\ y = 1

|| P[i: [1..N]] ::
[
   local z: int
   loop forever do
   [
      l0: noncritical;
      l1: (z, y) := (y, y + 1);
      l2: await z = x;
      l3: critical;
      l4: x:= x + 1
   ]
]

SPEC


value I, J: [1..N]

PROPERTY behavior1:
   [] (x <= y /\
       (Forall i: [1..N] . l2[i] --> x <= z[i] /\ z[i] < y) /\
       (Forall i: [1..N] . l{3,4}[i] --> x = z[i] /\ z[i] < y) /\
       (Forall i, j: [1..N] . l{2,3,4}[i] /\ l{2,3,4}[j] /\ z[i] = z[j] --> i = j))

PROPERTY behavior2:
   [] Forall k: int . x <= k /\ k < y --> Exists i: [1..N] . l{2,3,4}[i] /\ z[i] = k

PROPERTY mutual_exclusion:
   [] Forall i, j: [1..N] . l3[i] /\ l3[j] --> i = j

PROPERTY one_bounded_overtaking:
   l2[I] ==> !l3[J] Awaits l3[J] Awaits !l3[J] Awaits l3[I]

PROPERTY accessibility:
   l1[I] ==> <> l3[I]