dekker_n.cub

(*
   Generalization of Dekker mutual exclusion algorithm by Alain J. Martin from
   A new generalization of dekker’s algorithm for mutual
   exclusion. Inf. Process. Lett., 23(6) :295–297, Dec. 1986.

          --------------------------------------
          p(i) =
   NCS:       while true do
                  x(i) := true;
   LOOP:          while (exists j ≠ i. x(j)) do
   AWAIT:             x(i) := false;      
                      await [ t = 0 or t = i ];
   TURN:              t := i;
                      x(i) := true;
                  done;
   CS:            // CS(i);
                  x(i) := false;
                  t := 0;
              done
          --------------------------------------

   Translated from MCMT v2 model.
*)


type location = NCS | LOOP | AWAIT | TURN | CS

array P[proc] : location
array X[proc] : bool

var T : proc
var T_set : bool

init (i) { T_set = False && X[i] = False && P[i] = NCS }

unsafe (i j) { P[i] = CS && P[j] = CS }


transition start (i)
requires { P[i] = NCS }
{
  P[i] := LOOP;
  X[i] := True;  
}


transition wait (i j)
requires { P[i] = LOOP && X[j] = True }
{
  P[i] := AWAIT;
  X[i] := False;  
}


transition enter (i)
requires { P[i] = LOOP && forall_other j. X[j] = False }
{
  P[i] := CS;
}


transition awaited_1 (i)
requires { P[i] = AWAIT && T_set = False }
{
  P[i] := TURN;
}

transition awaited_2 (i)
requires { P[i] = AWAIT && T_set = True && T = i }
{
  P[i] := TURN;
}


transition turn (i)
requires { P[i] = TURN }
{
  P[i] := LOOP;
  X[i] := True;
  T_set := True;
  T := i;
}


transition loop (i)
requires { P[i] = CS }
{
  P[i] := NCS;
  X[i] := False;
  T_set := False;
}