module main {
    // Define the shared variable
    var x : int;

    // Initialize the shared variable
    init {
        x = 3;
    }

    // Procedure for Action A: x := 2 * x
    procedure actionA()
    modifies x;
    {
        x = 2 * x;
    }

    // Procedure for Action B: x := x + 1
    procedure actionB()
    modifies x;
    {
        x = x + 1;
    }

    // Next state relation using non-deterministic choice to simulate interleaving
    next {
        if (*) {
            call actionA();
        } else {
            call actionB();
        }
    }

    // Example safety property: x should remain non-negative
    invariant x_non_negative: x >= 0;

    // Control block for simulation and checking
    control {
        v = simulate 10;
        print_trace;
        check;
    }
}
