
module process
{
  type action_t = enum { LOAD, INC, STORE };
  var x : int;

  procedure P1()
  {
    var i : int;
    x := 0;
    for i := 1 to 10 do
    {
      call LOAD(x);
      call INC(x);
      call STORE(x);
    }
  }

  procedure P2()
  {
    var i : int;
    x := 0;
    for i := 1 to 10 do
    {
      call LOAD(x);
      call INC(x);
      call STORE(x);
    }
  }

  procedure P3()
  {
    var i : int;
    x := 0;
    for i := 1 to 10 do
    {
      call LOAD(x);
      call INC(x);
      call STORE(x);
    }
  }

  procedure LOAD(x : int)
  {
    assume(true); // Placeholder for load action
  }

  procedure INC(x : int)
  {
    x := x + 1;
  }

  procedure STORE(x : int)
  {
    assume(true); // Placeholder for store action
  }
}

module main
{
  var x : int;

  instance p1 : process.P1();
  instance p2 : process.P2();
  instance p3 : process.P3();

  init
  {
    x := 0;
  }

  next
  {
    next(p1);
    next(p2);
    next(p3);
  }

  property terminal_value_x_is_2()
  {
    x == 2;
  }

  control
  {
    check(terminal_value_x_is_2());
  }
}
