int c=1;
int x1=0;
int x2=0;


#define PROC(NAME, MAX, VAR) active proctype NAME() {\
Q: if\
::  atomic {c<MAX;VAR = c;}  goto R;\
fi;\
R: if\
:: VAR = VAR+c; goto S;\
fi;\
S: if\
:: c = VAR; goto Q;\
fi;\
}

PROC(P_0, 400, x1)

PROC(P_1, 400, x2)

never
{
again:
  if
  ::true; goto again;
  ::c==749;
  fi;
}