## 2.2  The Heater

Consider the problem of a system which control a gas heater as informally depicted in figure 2.1.

The heater front has a green light indicating a normal functioning whereas the red light is turned on when some problem has occurred (security stop). In that case, the heater is stopped and it can be restarted by pushing a restart button. Moreover, a rotating button allows the user to indicate the expected temperature of the water.

The controller has thus the following inputs.

• `restart` is used to restart the heater.
• `expected_temp` is the expected temperature of the water. The heater is expected to maintain this temperature.
• `actual_temp` is the actual temperature of the water measured by a sensor.
• `light_on` indicates that the light is on (that is, the gas is burning)
• `millisecond` is a boolean flow given the clock of the system.

The outputs of the controller are the following:

• `open_light` opens the light command.
• `open_gas` opens the valve for the gas.
• `ok` indicate the status of the heater (controlling the green light) whereas `nok` indicates a problem (thus controlling the red light). Only the `restart` button can restart the heater.

The purpose of the controller is to keep the water temperature close to the expected temperature. Moreover, when this temperature must be heated, the controller turns on the gas and light for at most `500` millisecond. When the light is on, only the gas valve is maintained open. If there is no light after `500` millisecond, it stops for `100` millisecond and start again. If after three tests, there is still no light, the heater is blocked on a security stop. Only pushing the `restart` button allows to start again the process.

We start with the definition of a few scalar constants and two auxiliary functions.

```let static low = 4
let static high = 4

let static delay_on = 500 (* in miliseconds *)
let static delay_off = 100

(* [count d t] returns [true] when [d] occurrences of [t] has been received *)
let node count d t = ok where
rec ok = cpt = 0
and cpt = d -> if t & not (pre ok) then pre cpt - 1 else pre cpt

let node edge x = false -> not (pre x) & x
```

The following node decides weather the heater must be turn on. We introduce an hysteresis mechanism to avoid oscillation. `low` and `high` are two threshold. The first version is a purely data-flow one whereas the second one (which is equivalent) uses the automaton construction.

```(* controling the heat *)
(* returns [true] when [expected_temp] does not agree with [actual_temp] *)
let node heat expected_temp actual_temp = ok where
rec ok = if actual_temp <= expected_temp - low then true
else if actual_temp >= expected_temp + high then false
else false -> pre ok

(* the same function using two modes *)
let node heat expected_temp actual_temp = ok where
rec automaton
False ->
do ok = false
unless (actual_temp <= expected_temp - low) then True
| True ->
do ok = true
unless (actual_temp >= expected_temp + high) then False
end
```

Now, we define a node which turns on the light and gas for 500 millisecond then turn them off for 100 millisecond and restarts.

```(* a cyclic two mode automaton with an internal timer *)
(* [open_light = true] and [open_gas = true] for [delay_on millisecond] *)
(* then [open_light = false] and [open_gas = false] for *)
(* [delay_off millisecond] *)
let node command millisecond = (open_light, open_gas) where
rec automaton
Open ->
do open_light = true
and open_gas = true
until (count delay_on millisecond) then Silent
| Silent ->
do open_light = false
and open_gas = false
until (count delay_off millisecond) then Open
end
```

The program which control the aperture of the light and gas is written below:

```(* the main command which control the opening of the light and gas *)
let node light millisecond on_heat on_light = (open_light, open_gas, nok) where
rec automaton
Light_off ->
do nok = false
and open_light = false
and open_gas = false
until on_heat then Try
| Light_on ->
do nok = false
and open_light = false
and open_gas = true
until (not on_heat) then Light_off
| Try ->
do
(open_light, open_gas) = command millisecond
until light_on then Light_on
until (count 3 (edge (not open_light))) then Failure
| Failure ->
do nok = true
and open_light = false
and open_gas = false
done
end
```

Finally, the main function connects the two parts.

```(* the main function *)
let node main millisecond restart expected_temp actual_temp on_light =
(open_light, open_gas, ok, nok) where
rec reset
on_heat = heat expected_temp actual_temp
and
(open_light, open_gas,nok) = light milisecond on_heat on_light
and
ok = not nok
every restart
```

Supposing that the program is written in a file `heater.ls`, the program can be compiled by typing:

```% lucyc -s main heater.ls
```

which produces files `heater.ml` and `main.ml`, the later containing the transition function for the node `main`.