Write UCLID5 code to complete the following task.

> A major use of energy worldwide is in heating, ventilation, and air conditioning (HVAC) systems. Model a thermostat with hysteresis, which regulates temperature to maintain a setpoint, or target temperature. It should have a state for heating and cooling. Suppose the setpoint is 20 degrees Celsius. If the heater is on, then the thermostat allows the temperature to rise past the setpoint to 22 degrees. If the heater is off, then it allows the temperature to drop past the setpoint to 18 degrees. There is a single input temperature with type real and two pure outputs heatOn and heatOff. These outputs will be present only when a change in the status of the heater is needed (i.e., when it is on and needs to be turned off, or when it is off and needs to be turned on). Use the variable names temp, heatOn and heatOff.

Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
