/* Dekker's algorithm, translated from the
   Promela version below */

want(0)=false. want(1)=false. turn=0.
cs(0)=false. cs(1)=false.
p(0), p(1).
p(K) :- p(K,do1).

p(K,do1), want(K2)=$x :- unary($x),K2=:=K |
  want(K)=true, p(K,do2).

p(K,do2), want(K2)=false :- K2=\=K |
  p(K,cs1), want(K2)=false.
p(K,do2), want(K2)=true  :- K2=\=K |
  p(K,if),  want(K2)=true.

p(K,if),turn=K2 :- K2=:=K | p(K,do2),turn=K.
p(K,if),turn=K2,want(K3)=$x :-
  K2=\=K, K3=:=K, unary($x) |
  p(K,wait), want(K)=false, turn=K2.

p(K,wait), want(K2)=$x, turn=K3 :-
  unary($x), K2=:=K, K3=:=K |
  p(K,do2), want(K)=true, turn=K.

p(K,cs1), cs(K2)=$x :- unary($x), K2=:=K |
  p(K,cs2), cs(K)=true.

p(K,cs2), cs(K2)=$x, want(K3)=$y, turn=$z :-
  K2=:=K, K3=:=K, unary($x), unary($y), $z1=1-$z |
  p(K,do1), cs(K)=false, want(K)=false, turn=$z1.

% /* Dekker's algorithm from the jSpin distribution */
% 
% bool want[2], cs[2];
% byte turn;
% 
% want[1] = false, want[2] = false,
% turn = 1,
% cs[1] = false, cs[1] = false,
% 
% active proctype p(Me) {
% /*do1*/
%     do
%     ::  want[Me] = true;
% /*do2*/ do
%         :: !want[1-Me] -> break;
%         :: else ->
% /*if*/      if
%             :: (turn == Me)
%             :: (turn == 1-Me) ->
%                 want[Me] = false;
% /*wait*/              (turn == Me);
%                 want[Me] = true	
%             fi
%         od;
% /*cs1*/ cs[Me] = true;
%         assert (!(cs1 && cs2));
% /*cs2*/ cs[Me] = false;
%         want[Me] = false;
%         turn = 1-Me
%     od
% }
% 
% p(0), p(1).
