
module main {
  var x : int;

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

  process P1 {
    var i : int;
    i = 1;
    do
      LOAD(x);
      INC(x);
      STORE(x);
      i = i + 1;
    od
  }

  process P2 {
    var i : int;
    i = 1;
    do
      LOAD(x);
      INC(x);
      STORE(x);
      i = i + 1;
    od
  }

  process P3 {
    var i : int;
    i = 1;
    do
      LOAD(x);
      INC(x);
      STORE(x);
      i = i + 1;
    od
  }

  init {
    x = 0;
  }

  next {
    P1;
    P2;
    P3;
  }

  invariant x_terminal_value: x == 2;
}
