#define N 5
#define NULL 255
byte b0, b1, b2, b3, b4;
byte x=NULL;
byte y=NULL;
bit inCS0, inCS1, inCS2, inCS3, inCS4;

#define PROC(NAME, B, ID, COMP, INCS)\
active proctype NAME()\
{\
byte j=0;\
NCS: if\
:: B = 1; goto q1;\
fi;\
CS: if\
:: y = NULL; goto e1;\
fi;\
q1: if\
:: x = ID; goto q2;\
fi;\
q2: if\
:: atomic {y!=NULL;B = 0;}  goto q22;\
:: y==NULL; goto p;\
fi;\
q22: if\
:: atomic{y==NULL;INCS=0;} goto NCS;\
fi;\
p: if\
:: y = ID; goto q3;\
fi;\
q3: if\
:: atomic{x==ID;INCS=1;} goto CS;\
:: atomic{x!=ID;B = 0;j = 0;}  goto q4;\
fi;\
q4: if\
::  atomic\
    {\
      if\
      ::j==0 && b0==0;\
      ::j==1 && b1==0;\
      ::j==2 && b2==0;\
      ::j==3 && b3==0;\
      ::j==4 && b4==0;\
      fi;\
      j = j+1;\
    } goto q4;\
:: j==N; goto q5;\
fi;\
q5: if\
:: atomic{y==COMP;INCS=1;} goto CS;\
:: atomic{y==NULL;INCS=0;} goto NCS;\
fi;\
e1: if\
:: atomic{B = 0;INCS=0;} goto NCS;\
fi;\
}



PROC(P_0, b0, 0, 0, inCS0)

PROC(P_1, b1, 1, 1, inCS1)

PROC(P_2, b2, 2, 2, inCS2)

PROC(P_3, b3, 3, 3, inCS3)

PROC(P_4, b4, 4, 4, inCS4)

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