module main {
    // Shared variable
    var x : int;

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

    // Define actions A and B
    procedure actionA()
    modifies x;
    {
        x = 2 * x;
    }

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

    // Non-deterministic choice to simulate interleaving of A and B
    next {
        if (*) {
            call actionA();
            call actionB();
        } else {
            call actionB();
            call actionA();
        }
    }

    // Control block for checking and printing results
    control {
        v = unroll(2); // Unroll twice to cover all interleavings
        check;
        print_results;
    }
}
