bool x,y;
byte mutex;

active proctype X() {
lab1: 
 y = 1;
  x == 0;
  mutex ++;
  mutex --;
  y = 0;
goto lab1;
}

active proctype Y() {
 lab2: 
  x = 1;
  y == 0;
  mutex ++;
  mutex --;
  x = 0;
goto lab2;
}

active proctype monitor() {
  assert(mutex != 2);
}