Consider the problem of a system which control a gas heater as informally depicted in figure 2.1.
Figure 2.1: The heater
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
.