
module P1
{
  var x : int;

  procedure process()
  {
    for i := 1 to 10 do
    {
      LOAD(x);
      INC(x);
      STORE(x);
    }
  }
}

module P2
{
  var x : int;

  procedure process()
  {
    for i := 1 to 10 do
    {
      LOAD(x);
      INC(x);
      STORE(x);
    }
  }
}

module P3
{
  var x : int;

  procedure process()
  {
    for i := 1 to 10 do
    {
      LOAD(x);
      INC(x);
      STORE(x);
    }
  }
}

module main
{
  var x : int;

  P1.process();
  P2.process();
  P3.process();

  init {
    x = 0;
  }

  next {
    call P1.process();
    call P2.process();
    call P3.process();
  }

  property has_terminal_value_two {
    x == 2;
  }
}
