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