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 }