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

    // Initialize x to 3
    init {
        x = 3;
    }

    // Define the actions
    procedure actionA() {
        x = 2 * x;
    }

    procedure actionB() {
        x = x + 1;
    }

    // Model non-deterministic choice between actions
    next {
        if (*) {
            call actionA();
        } else {
            call actionB();
        }
    }

    // Optionally define invariants or properties to check
    invariant x_non_negative: x >= 0;

    control {
        // Set up the control block for simulation or verification
        v = simulate(10); // simulate for 10 steps
        print_results;
    }
}
