c
module thermostat
{
  type state_t = enum { HEATING, COOLING };

  var state : state_t;
  input temperature : real;
  output heatOn : boolean;
  output heatOff : boolean;

  const setpoint : real = 20.0;
  const upperThreshold : real = 22.0;
  const lowerThreshold : real = 18.0;

  init {
    state = HEATING;
    heatOn = false;
    heatOff = false;
  }

  next {
    if (state == HEATING) {
      if (temperature >= upperThreshold) {
        heatOn = false;
      } else if (temperature <= setpoint) {
        heatOn = true;
      }
    } else {
      if (temperature <= lowerThreshold) {
        heatOff = false;
      } else if (temperature >= setpoint) {
        heatOff = true;
      }
    }

    state' = (temperature >= setpoint) ? HEATING : COOLING;
  }
}

module main
{
  var temp : real;
  var heatOn : boolean;
  var heatOff : boolean;

  instance t : thermostat(temperature: temp, heatOn: heatOn, heatOff: heatOff);

  init {
    temp = 20.0;
  }

  next {
    temp := nondet_real();
    next(t);
  }

  control {
    v = unroll(5);
    check;
    print_results;
  }
}
