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

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

    // Define the non-deterministic choice for actions
    procedure action()
    modifies x;
    {
        if (*) {
            x = 2 * x; // Action A
        } else {
            x = x + 1; // Action B
        }
    }

    // Main transition system
    next {
        call action();
    }

    // Example safety property: check if x remains positive
    invariant x_positive: x > 0;

    // Control block for model checking
    control {
        v = unroll(5); // Unroll the transition system 5 times
        check;
        print_results;
    }
}
