
module main {
  type mem_val_t;
  var x : mem_val_t;
  
  init {
    x = 0;
  }

  procedure LoadX() returns (y: mem_val_t) {
    y = x;
  }

  procedure IncX(y: mem_val_t) returns (z: mem_val_t) {
    z = y + 1;
  }

  procedure StoreX(y: mem_val_t) {
    x = y;
  }

  procedure OneRound() {
    var y : mem_val_t;
    var z : mem_val_t;
    y = LoadX();
    z = IncX(y);
    StoreX(z);
  }

  procedure P1() {
    for i in 1 .. 10 {
      OneRound();
    }
  }

  procedure P2() {
    for i in 1 .. 10 {
      OneRound();
    }
  }
  
  procedure P3() {
    for i in 1 .. 10 {
      OneRound();
    }
  }

  control {
    parallel {
      P1();
      P2();
      P3();
    }
  }

  safety property x_equals_2 {
    x == 2
  }
}