1.6  Real Time versus Logical Time

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
   | 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:

val after : int * bool -D-> bool val blink_reset : bool * int * int * bool -D-> bool

Does after(n, second) really give a delay of n real-time seconds? No, for three reasons (see also [7]):

  1. second is a Boolean stream. No hypothesis is made or ensured by the compiler about the actual real-time duration between two occurrences of true in the stream. It is up to the implementation to ensure that second correctly approximates a real second.
  2. The counting of instants in the expression after(n, t) is only performed when the expression is active, that is, it returns true when n occurrences of the value true have been observed. Instantiating blink_reset within a branch of an automaton or match may skew the relation between logical and real time.
  3. Even given an ‘accurate’ second signal and ignoring the possibility of suspension at a higher-level, the expression after(n, second) still only gives a delay in the interval (n−1, n] seconds. This is because it counts ticks, not the ‘spaces’ between ticks. If restart occurs just before but not simultaneously with second, then the real-time delay will be less than n seconds.

In the discrete-time programs of this chapter, time is not real and absolute but rather logical and local.