module main {
    var x : int;

    init {
        x = 3;
    }

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

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

    // Define a nondeterministic scheduler that either executes action A or action B
    next {
        if (*) {
            call action_A();
        } else {
            call action_B();
        }
    }

    control {
        // Unroll the system for a few steps to observe behavior
        v = unroll(5);
        check;
        print_results;
        v.print_cex(x);
    }
}
