module PetersonModule {
  var b1: boolean;
  var b2: boolean;
  var x: integer;

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

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

  next {
    call step();
  }
}
