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.
restartis used to restart the heater.
expected_tempis the expected temperature of the water. The heater is expected to maintain this temperature.
actual_tempis the actual temperature of the water measured by a sensor.
light_onindicates that the light is on (that is, the gas is burning)
millisecondis a boolean flow given the clock of the system.
The outputs of the controller are the following:
open_lightopens the light command.
open_gasopens the valve for the gas.
okindicate the status of the heater (controlling the green light) whereas
nokindicates a problem (thus controlling the red light). Only the
restartbutton 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
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
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.
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
program can be compiled by typing:
% lucyc -s main heater.ls
which produces files
main.ml, the later
containing the transition function for the node