Previous Up Next

1.8  State Machines and Signals

In the automata we have considered so far, conditions on transitions are boolean expressions. The language provides a more general mechanism allowing to test (and access) signals on transitions.

Using signals, we can reprogram the mouse controller in the following way.

type e = Simple | Double

let node controler click top = o where
  automaton
    Await ->
     do until click then One
  | One ->
     do unless click then Emit Double
     unless (counting top = 4) then Emit Simple
  | Emit(x) ->
     do emit o = x
     until true then Await
  end

val controler :  bool -> bool => e sig
val controler :: ’a -> ’a -> ’a sig

Note that nothing is emitted in states Await and One. It should normally raise an error (in the existing form of automata). By writting emit o = x, we state that o is a signal and not a regular stream. We do not impose o to be defined in every branch (and to complement it with its last value). Here, the signal o is only emitted in state Emit. Otherwise, it is considered to be absent.

The use of signals combined with sum type has some advantage here with respect to the use of boolean variables in the previous version of the mouse controller. By construction, only three values are possible for the output of the system: o can be Simple, Double or absent. In the previous version, a fourth case corresponding to the boolean value simple & double was possible, even though it does not make sense.

1.8.1  Pattern Matching over Signals

Now, we must consider how signals are accessed. We generalize conditions to be signal patterns as provided by the present statement.

Let us consider a system with two input signals low, high and an output integer stream o.

let node switch low high = o where
  rec automaton
        Init -> do o = 0 until low(u) then Up(u)
      | Up(u) ->
          do o = last o + u
          until high(v) then Down(v)
      | Down(v) ->
          do o = last o - v
          until low(w) then Up(w)
      end

val switch :  ’a sig -> ’a sig => ’a
val switch :: ’a sig -> ’a sig -> ’a

The condition until low(w) says: await for the presence of the signal low with some value w. Then go to the parameterized state Up(w).

The right part of a pre-emption condition is of the form e(p) where e is an expression of type t sig and p stands for a pattern of type t. The condition is a binder: the pattern p is bound with the value of the signal at the instant where e is present. In the above example, it introduces the variable w. It is also possible to test for the presence of a signal as well as the validity of a boolean condition. For example:

let node switch low high = o where
  rec automaton
    Init -> do o = 0 until low(u) then Up(u)
  | Up(u) ->
      let rec timeout = 0 -> pre timeout + 1 in
      do o = last o + u
      until high(v) & (timeout > 42) then Down(v)
  | Down(v) ->
      let rec timeout = 0 -> pre timeout + 1 in
      do o = last o - v
      until low(w) & (timeout > 42) then Up(w)
  end

val switch :  ’a sig -> ’a sig => ’a
val switch :: ’a sig -> ’a sig -> ’a

The system has the same behavior except that the presence of high in the Up state is only taken into account when the timeout stream has reached the value 42.

Finally, we can write a new version of the mouse controller where all the values are signals.

type e = Simple | Double

let node counting e = o where
  rec o = if ?e then 1 -> pre o + 1 else 0 -> pre o

let node controler click top = e where
  automaton
    Await ->
     do until click(_) then One
  | One ->
     do unless click(_) then Emit Double
     unless (counting top = 4) then Emit Simple
  | Emit(x) ->
     do emit e = x
     then Await
  end

val controler :  ’a sig -> ’b sig => ’c sig
val controler :: ’a sig -> ’a sig -> ’a sig

1.8.2  The derived operator await/do

The operator await/do is a built-in operator which allows to await for a the presence of a signal. This is a short-cut for a two states automaton. For example:

(* emits nothing while x is not present *)
(* then start counting from the received value *)
let node counting x = o where
  automaton
    Await -> do unless x(v) then Run(v)
  | Run(v) -> let rec cpt = v -> pre cpt + 1 in
       do emit o = cpt done
  end

This can be written as:

let node counting x = 
  await x(v) do
  let rec cpt = v -> pre cpt + 1 in
  cpt

val counting :  int sig => int
val counting :: ’a sig -> ’a

We end with a function which awaits for the n-th occurrence of a signal and returns a signal made of the value received at the instant. We write it in two different ways:

let node nth n s = o where
  rec cpt = if ?s then 1 -> pre cpt + 1 else 0 -> pre cpt
  and o = await s(x) & (cpt = n) do x

Awaiting the second occurrence of a signal s can be written:

let node second s = await (nth 2 s)(v) do v

Previous Up Next