We close the chapter on synchronous programming with an example real-time controller that tracks the passage of time using counters that then influence the running mode. This example highlights the difference between the idea of logical time considered thus far and that of real-time.
Consider a light that blinks according to the specification:
Repeat the following behavior indefinitely: Turn a light on for n seconds and then off for m seconds. Allow it to be restarted at any instant.
One way to start implementing this specification is to define a boolean signal called second that is true at every occurrence of a second, whatever that may mean, and false otherwise. We then define a node called after(n, t) that returns true when n true values are counted on t. This is then instantiated twice in a node called blink_reset containing an automaton with two modes wrapped by a reset construct.
let node after(n, t) = (cpt >= n) where rec tick = if t then 1 else 0 and ok = cpt >= n and cpt = tick -> if pre ok then n else pre cpt + tick let node blink_reset (restart, n, m, second) = x where reset automaton | On -> do x = true until (after(n, second)) then Off | Off -> do x = false until (after(m, second)) then On every restart
The type signatures inferred by the compiler are:
Does after(n, second) really give a delay of n real-time seconds? No, for three reasons (see also ):
In the discrete-time programs of this chapter, time is not real and absolute but rather logical and local.