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

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

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

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

    // Define the transition system with non-deterministic choice of action order
    next {
        if (*) {
            call action_A();
            call action_B();
        } else {
            call action_B();
            call action_A();
        }
    }

    // Example safety property (optional, for demonstration)
    // Check if x reaches a specific value; adjust the value as needed for your checks
    invariant x_value_check : (x == 7) || (x == 8);

    // Control block for execution and verification
    control {
        // Unroll the transition system twice to cover all interleavings
        v = unroll(2);
        check;
        print_results;
    }
}
