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;
        run P1 || P2 || P3;
    }

    property halt_with_x_2 {
        x == 2;
    }
}
