module Module {
  type Dom = integer;

  var b1_temp: boolean;
  var b2_temp: boolean;
  var b1: boolean;
  var b2: boolean;
  var x: Dom;

  init {
    b1 = false;
    b2 = false;
    x = 1;

  }
  procedure step()
    modifies b2_temp;
    modifies b1;
    modifies x;
    modifies b1_temp;
    modifies b2;
  {
    b1_temp = b1;
    b2_temp = b2;
    if (b1_temp && (x == 2)) {
      b1 = false;
    } else {
      if (b2_temp && (x == 1)) {
        b2 = false;
      }
    }
    if (!b1_temp && !b2_temp) {
      b1 = (if (x == 2) then true else false);
      b2 = (if (x == 1) then true else false);
    } else {
      if (b1_temp && b2_temp) {
        if (x == 1) {
          b1 = false;
        } else {
          if (x == 2) {
            b2 = false;
          }
        }
      }
    }
    if (!b1_temp && !b2_temp) {
      if (x == 1) {
        x = 2;
      } else {
        if (x == 2) {
          x = 1;
        }
      }
    }
  }

  next {
    call step();
  }
}
