module main {
    var temp : int; // temperature in degrees Celsius
    var heatOn : boolean; // heater state - on or off
    var heatOff : boolean; // heater state - on or off
    var time : int; // time elapsed in seconds

    init {
        assume(temp <= 20); // initial temperature condition
        heatOn = true;
        heatOff = false;
        time = 0;
    }

    transition {
        if (heatOn) {
            if (time < 30) {
                time := time + 1;
            } else {
                heatOn := false;
                heatOff := true;
                time := 0;
            }
        } else if (heatOff) {
            if (time < 120) {
                time := time + 1;
            } else {
                heatOn := (temp <= 20);
                heatOff := !heatOn;
                time := 0;
            }
        }
    }
}
