module main {
  const N = 10;
  var x: integer;

  procedure LOAD() modifies x;
  procedure INC() modifies x;
  procedure STORE() modifies x;

  process P1 {
    var i: integer;
    i = 0;
    do
      call LOAD();
      call INC();
      call STORE();
      i = i + 1;
    od
  }

  process P2 {
    var i: integer;
    i = 0;
    do
      call LOAD();
      call INC();
      call STORE();
      i = i + 1;
    od
  }

  process P3 {
    var i: integer;
    i = 0;
    do
      call LOAD();
      call INC();
      call STORE();
      i = i + 1;
    od
  }

  init {
    x = 0;
  }

  property halts {
    exists i: integer :: i < N && x == 2;
  }
}
