bool x,y;
byte mutex;

actoive proctype X() {
  y = 1;
  x == 0;
  mutex ++;
  mutex --;
  y = 0;
}

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

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