bool turn, flag[2];
byte ncrit;

active [2] proctype user()
{	byte r;

        assert(_pid == 0 || _pid == 1);
again:
        flag[_pid] = 1;
        turn = _pid;

loop:	r = flag[1 - _pid];
	if	/* the evaluation is split into two separate steps */
	:: r != 0 -> goto loop
	:: else ->
		r = turn;
		if
		:: r != 1 - _pid -> goto loop
		:: else
		fi
	fi;
 
      ncrit++;
      assert(ncrit == 1);     /* critical section */
      ncrit--;

      flag[_pid] = 0;
      goto again
}