#define ERROR <
#define NO_ERROR >
#define COMP ERROR
#define NUM_PROCS 4
#define MAX 12

byte choosing0, choosing1, choosing2, choosing3;
byte number0, number1, number2, number3;
bit inCS0, inCS1, inCS2, inCS3;

#define PROC(NAME, ID, CHOOSING, NUMBER, INCS, ERROR_FIELD) active proctype NAME() {\
byte j=0;\
byte max=0;\
\
NCS: if\
::  atomic {CHOOSING = 1;j = 0;max = 0;}  goto choose;\
fi;\
choose: if\
::  atomic {j==0 && j<NUM_PROCS && number0>max;max = number0;j = j+1;}  goto choose;\
::  atomic {j==1 && j<NUM_PROCS && number1>max;max = number1;j = j+1;}  goto choose;\
::  atomic {j==2 && j<NUM_PROCS && number2>max;max = number2;j = j+1;}  goto choose;\
::  atomic {j==3 && j<NUM_PROCS && number3>max;max = number3;j = j+1;}  goto choose;\
::  atomic {j==0 && j<NUM_PROCS && number0<=max;j = j+1;}  goto choose;\
::  atomic {j==1 && j<NUM_PROCS && number1<=max;j = j+1;}  goto choose;\
::  atomic {j==2 && j<NUM_PROCS && number2<=max;j = j+1;}  goto choose;\
::  atomic {j==3 && j<NUM_PROCS && number3<=max;j = j+1;}  goto choose;\
::  atomic {j==NUM_PROCS && max<MAX;NUMBER = max+1;j = 0;CHOOSING = 0;}  goto for_loop;\
fi;\
for_loop: if\
:: j==0 && j<NUM_PROCS && choosing0==0; goto wait;\
:: j==1 && j<NUM_PROCS && choosing1==0; goto wait;\
:: j==2 && j<NUM_PROCS && choosing2==0; goto wait;\
:: j==3 && j<NUM_PROCS && choosing3==0; goto wait;\
:: atomic{j==NUM_PROCS; INCS=1;} goto CS;\
fi;\
wait: if\
::  atomic{j==0 && (number0==0 || (number0 ERROR_FIELD NUMBER) || (number0==NUMBER && ID<=j));j = j+1;}  goto for_loop;\
::  atomic{j==1 && (number1==0 || (number1 ERROR_FIELD NUMBER) || (number1==NUMBER && ID<=j));j = j+1;}  goto for_loop;\
::  atomic{j==2 && (number2==0 || (number2 ERROR_FIELD NUMBER) || (number2==NUMBER && ID<=j));j = j+1;}  goto for_loop;\
::  atomic{j==3 && (number3==0 || (number3 ERROR_FIELD NUMBER) || (number3==NUMBER && ID<=j));j = j+1;}  goto for_loop;\
fi;\
CS: if\
:: atomic{NUMBER=0; INCS=0;} goto NCS;\
fi;\
}

PROC(P_0, 0, choosing0, number0, inCS0, COMP)

PROC(P_1, 1, choosing1, number1, inCS1, COMP)

PROC(P_2, 2, choosing2, number2, inCS2, COMP)

PROC(P_3, 3, choosing3, number3, inCS3, COMP)

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