module main {
    var warn : boolean;
    var noWarn : boolean;
    var time : int;
    var ignition : boolean;
    var buckled : boolean;

    init {
        warn = false;
        noWarn = true;
        time = 0;
        ignition = false;
        buckled = true;
    }

    next {
        if (ignition && !buckled) {
            warn = true;
            noWarn = false;
        } else if (!ignition || buckled) {
            warn = false;
            noWarn = true;
        }

        if (warn && time < 30) {
            time = time + 1;
        } else {
            warn = false;
        }
    }

    invariant beeper_time : (time <= 30);
    invariant warn_light_correct : (warn == !buckled);
}
