
module main {
    var x : int;
    type action_t = enum {IDLE, ACTION_A, ACTION_B};
    var action : action_t;

    init {
        x = 3;
        action = IDLE; // It's important to initialize 'action' in init
    }

    next(action) {
        action' = nondet(action_t); // Deterministic assignment
    }

    next {
        case
        action == ACTION_A: x' = 2 * x;
        action == ACTION_B: x' = x + 1;
        action == IDLE: x' = x;
        esac;
    }

    control {
        while (*) {
            if (*) {
                action = ACTION_A;
            } else {
                action = ACTION_B;
            }
        }
    }
}