module ThermostatModule {
  var temp: real;
  var heatOn: boolean;
  var heatOff: boolean;
  var time: real;

  init {
    heatOn = (temp <= 20.0);
    heatOff = !heatOn;
    time = 0.0;

  }
  next {
    if (time > 0.0) {
      time' = (time - 30.0);
    } else {
      if (time <= 0.0) {
        if (heatOn) {
          if (temp > 20.0) {
            heatOn' = false;
            heatOff' = true;
            time' = 120.0;
          }
        } else {
          if (temp <= 20.0) {
            heatOn' = true;
            heatOff' = false;
            time' = 30.0;
          }
        }
      }
    }

  }
  invariant spec: (heatOn && (time < 30.0));

}
