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(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(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(n, second)) then Off
   | Off -> do x = false until (after_n(m, second)) then On
 every restart

The type signatures inferred by the compiler are:

Does after_n(n, second) really give a delay of n real-time seconds? No, for two 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(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. This can be less than the number of occurrences of the value true of n. E.g., instantiating blink_reset within a branch of an automaton or match that is activated from time to time.

In this chapter, time is logical meaning that we count number of occurrences. We shall see in the next chapter how to connect it with physical time.