#define ERROR <=
#define NO_ERROR <
#define COMP NO_ERROR
#define N 3
byte pos0, pos1, pos2;
byte step0, step1, step2;
bit inCS0, inCS1, inCS2;

#define PROC(NAME, POS, INCS, ID)\
active proctype NAME()\
{\
byte j=0;\
byte k=0;\
NCS: if\
:: j = 1; goto wait;\
fi;\
CS: if\
:: atomic {POS = 0; INCS=0;} goto NCS;\
fi;\
wait: if\
::  atomic {j<N;POS = j;}  goto q2;\
::  atomic {j==N; INCS=1;} goto CS;\
fi;\
q2: if\
::  atomic\
{\
  if\
  :: j-1==0; step0 = ID;k = 0;\
  :: j-1==1; step1 = ID;k = 0;\
  :: j-1==2; step2 = ID;k = 0;\
  fi;\
}  goto q3;\
fi;\
q3: if\
::  atomic\
{\
  if\
  :: k==0 && k<N && (k==ID || pos0 COMP j);k = k+1;\
  :: k==1 && k<N && (k==ID || pos1 COMP j);k = k+1;\
  :: k==2 && k<N && (k==ID || pos2 COMP j);k = k+1;\
  fi;\
}  goto q3;\
::  atomic\
{\
  if\
  :: j-1==0 && (pos0!=ID || k==N);j = j+1;\
  :: j-1==1 && (pos1!=ID || k==N);j = j+1;\
  :: j-1==2 && (pos2!=ID || k==N);j = j+1;\
  fi;\
}  goto wait;\
fi;\
}

PROC(P_0, pos0, inCS0, 0)

PROC(P_1, pos1, inCS1, 1)

PROC(P_2, pos2, inCS2, 2)

never
{
again:
  if
  :: true; goto again;
  :: (inCS0 + inCS1 + inCS2)>1;
  fi;
}