Zélus provides hierarchical state machines that can be composed in parallel with regular equations or other state machines as well as arbitrarily nested. State machines are essentially taken as is from Lucid Synchrone and SCADE 6. They are compiled to data-flow equations .
In this tutorial, we first consider basic state machines where transition guards are limited to boolean expressions. We then consider two important extensions. The first is the ability to define state machines with parameterized states (section 1.4.3) and actions on transitions (section 1.4.9). The second is a more general form of transitions with signal matching and boolean expressions (section 1.4.11).
An automaton is a collection of states and transitions. Two kinds of transitions are provided: weak and strong. For each, it is possible to enter the next state by reset or by history. An important feature of state machines in Zélus is that only one set of equations is executed during any single reaction.
The following program contains a two state automaton with strong preemption, it returns false until x becomes true and then it returns true indefinitely.
let node strong x = o where automaton | S1 -> do o = false unless x then S2 | S2 -> do o = true done end
Each of the two states defines a value for the shared variable o. The keyword unless indicates a strong transition: the automaton stays in the state S1 as long as x is false, and o is defined by the equation o = false, but the instant that x becomes true, S2 becomes active immediately, and o is defined by the equation o = true. Thus, the following timeline holds:
The guards of strong transitions are tested before determining which state is active at an instant and executing its body.
The following program contains a two state automaton with weak preemption, it returns false at the instant that x becomes true and then it returns true indefinitely; it is like a Moore automaton.
let node expect x = o where automaton | S1 -> do o = false until x then S2 | S2 -> do o = true done end
This timeline of this program is shown below.
The guards of weak transitions are tested after executing the body of the current active state to determine the active state at the next instant.
We now consider a two state automaton that switches between two states whenever the input toggle is true.
let node weak_switch toggle = o where automaton | False -> do o = false until toggle then True | True -> do o = true until toggle then False end
For an example input stream, the timeline is:
The form with strong transitions follows.
let node strong_switch toggle = o where automaton | False -> do o = false unless toggle then True | True -> do o = true unless toggle then False end
Its behavior relative to the same input sequence differs.
In fact, for any boolean stream toggle the following property holds:
let node correct toggle = weak_switch toggle = strong_switch (false -> pre toggle)
The graphical representations of these two automata are shown in figure 1.3. The circles on the transition arrows distinguish weak transitions from strong ones: they graphically separate the actions of one instant from another. Since a weak transition is executed in the same instants as its source state, the circle is placed to separate it from its destination state. Since a strong transition is executed in the same instants as its destination state, the circle is placed to separate it from its source state.
Remark: The current version of Zélus does not permit arbitrary combinations of weak and strong transitions within an automaton as in Lucid Synchrone and SCADE 6. After much experience with automata, we think that such arbitrary mixes give programs that are difficult to understand. Future versions of Zélus may, however, allow a constrained mix of weak and strong transitions.
In the examples considered so far, each automaton had a finite set of states and transitions. It is also possible to define more general state machines with parameterized states, that is, states containing local values that are initialized on entry. Parameterized states are a natural way to pass information between states and to reduce the number of explicitly programmed states. Parameterized state machines lead to a style of programming that resembles the definition of mutually tail-recursive functions in ML. Yet they are not compiled into mutually recursive functions but into a single step function with a switch-like construct over the active state.
In the following function, the automaton waits in its initial state for the signal e. When e is present, its value is bound to v and the automaton transitions to the state Sustain(v), that is, to the state Sustain with parameter x set to v.
(* wait for e and then sustain its value indefinitely *) let node await e = o where automaton | Await -> do unless e(v) then Sustain(v) | Sustain(x) -> do emit o = x done end
The formal parameter x of the Sustain state can be used without restriction in the body of the state, and the variable v could just as well have been an expression.
As another example, the program below uses parameterized states to count the occurrences of x. It simulates an infinite state machine with states Zero, Plus(1), Plus(2), etcetera.
let node count x = o where rec o = 0 -> pre o + 1 let node count_in_an_automaton x = o where automaton | Zero -> do o = 0 until x then Plus(1) | Plus(v) -> do o = v until x then Plus(v+1) end
Gérard Berry’s ABRO example highlights the expressive power of parallel composition and preemption in Esterel. The specification is [5, §3.1]:
Emit an output O as soon as two inputs A and B have occurred. Reset this behavior each time the input R occurs.
We will implement this example in Zélus—replacing uppercase letters by lowercase ones5—but generalize it slightly by considering valued events.
As a first step, consider a function that implements the first part of the specification: it waits for occurrences of both a and b using the await node from section 1.4.3 and then emits the sum of their values.
let node abo (a, b) = o where present (await a)(v1) & (await b)(v2) -> do emit o = v1 + v2 done
This first version is readily extended to the full specification by putting it inside an automaton state with a self-looping (weak) transition that resets it when r is true.
let node abro (a, b, r) = o where automaton | S1 -> do present (await a)(v1) & (await b)(v2) -> do emit o = v1 + v2 done unless r then S1 end
A graphical version is shown in figure 1.4. The transition on r resets the computation within the state: all streams in abo a b, including those inside both await nodes, restart with their initial values.
Zélus also provides a specific reset/every primitive as a shortcut for such a one-state automaton. It combines a set of parallel equations (separated by ands). We could thus write:
let node strong_abro (a, b, r) = o where reset present (await a)(v1) & (await b)(v2) -> do emit o = v1 + v2 done every r
Except that reset/every is strongly preemptive; the body is reset before being executed at the instant the condition is true. There is no “weak reset” since one need only add a unit delay for the same effect. The following program implements the ABRO specification.
let node abro (a, b, r) = o where reset o = abo (a, b) every true fby r
Names may be declared local to a state. Such names can only be used inside the body of the state and in the guards of outgoing weak transitions.
The following program sums the integer sequence v and emits false until the sum has reached some value max. Then, it emits true for n instants.
let node consume (max, n, v) = status where automaton | S1 -> let rec c = v -> pre c + v in do status = false until (c = max) then S2 | S2 -> let rec c = 1 -> pre c + v in do status = true until (c = n) then S1 end
State S1 defines a local variable c that is used to compute the weak condition c = max without introducing any causality problems. Indeed, weak transitions only take effect in a subsequent reaction: they define the next state, not the current one. Moreover, there is no restriction on the kind of expressions appearing in conditions and they may, in particular, have some internal state. For example, the previous program can be rewritten as:
let node sum v = cpt where rec cpt = v -> pre cpt + v let node consume (max, n, v) = status where automaton | S1 -> do status = false until (sum v = max) then S2 | S2 -> do status = true until (sum 1 = n) then S1 end
The body of a state comprises (possibly empty) sequences of local declarations (with local/in), local definitions (with let/in), and definitions of shared variables (with do/until). As noted previously, weak conditions may depend on local names and shared names.
In weak preemptions, as in the example above, transition conditions are evaluated after the equations in the body have been evaluated. The untils in this example may not be replaced with unlesss because in strong preemptions the transition conditions are evaluated before the equations in the body and may not depend on them. Thus, writing
let node consume (max, n, v) = status where automaton | S1 -> let rec c = v -> pre c + v in do status = false unless (c = max) then S2 | S2 -> let rec c = 1 -> pre c + 1 in do status = true unless (c = n) then S1 end
causes the compiler to emit the message:
The variable c is not visible in the handler of the unless. The same problem occurs if c is declared as a local variable, as in the following program.
let node consume (max, n, v) = status where automaton | S1 -> local c in do c = v -> pre c + v and status = false unless (c = max) then S2 | S2 -> local c in do c = v -> pre c + v and status = true unless (c = n) then S1 end
In the previous examples, there is no communication between the values computed in each state. We now consider the following simple system, due to Maraninchi and Rémond , of two running modes.
let node two_states (i, min, max) = o where rec automaton | Up -> do o = last o + 1 until (o = max) then Down | Down -> do o = last o - 1 until (o = min) then Up end and init o = i
In the Up mode, the system continually increments some value by 1 and in the Down mode, it decrements the same value by the same amount. The transitions between these two modes are described by a two-state automaton whose behavior depends on the value computed in each mode. The system’s execution diagram is
|last o + 1||1||2||3||4||0||1||2||…|
|last o - 1||3||2||1||0||-1||…|
As for match/with and present, an implicit completion mechanism applies so that variables like o need not be explicitly defined in all automaton states. When an equation is not given, the shared variable keeps its previous values. In other words, an equation o = last o is assumed.
The initial automaton state can be used to define the values of variables that are shared across the other states. Such variables are considered to have a last value that can be accessed through the last operator. And, thanks to o = last o completion, explicit definitions can be omitted in other states.
let node two_states (i, min, max) = o where rec automaton | Init -> do o = i until (i > 0) then Up | Up -> do o = last o + 1 until (o = max) then Down | Down -> do o = last o - 1 until (o = min) then Up end
|last o + 1||0||0||0||1||2||3||4||0||1||2||…|
|last o - 1||0||0||0||3||2||1||0||-1||…|
As the initial state Init is only weakly preempted, o is necessarily initialized with the current value of i. Thus, last o is well defined in the remaining states. Replacing weak preemption by strong preemption results in an error.
let node two_states (i, min, max) = o where rec automaton | Init -> do o = i unless (i > 0) then Up | Up -> do o = last o + 1 unless (o = max) then Down | Down -> do o = last o - 1 unless (o = min) then Up end
As explained in section 1.4.5, the guards of strong transitions may not depend on variables computed in the current state. They may depend, however, on a shared memory last o, as in:
let node two_states (i, min, max) = o where rec init o = i and automaton | Init -> do o = i unless (i > 0) then Up | Up -> do o = last o + 1 unless (last o = max) then Down | Down -> do o = last o - 1 unless (last o = min) then Up end
giving the same execution diagram as before:
|last o + 1||0||0||0||1||2||3||4||0||1||2||…|
|last o - 1||0||0||0||3||2||1||0||-1||…|
An initial state may be parameterized if an explicit initialization clause is added to the automaton. For example, the following two state automaton starts in state Run(incr) with incr initialized to the first value of i0.
let node two_states(i0, idle, run) = o where rec automaton | Run(incr) -> do o = 0 fby o + incr until idle() then Idle | Idle -> do until run(incr) then Run(incr) init Run(i0)
By default, the computations within an automaton state are reset when it is entered. So, for instance, the counters in the states of the example below are reset on every transition.
let node time_restarting c = (x, y) where rec automaton | Init -> do x = 0 and y = 0 then S1 | S1 -> do x = 0 -> pre x + 1 until c then S2 | S2 -> do y = 0 -> pre y + 1 until c then S1 end
Giving the execution trace (where we write F for false and T for true):
Note that the transition from the initial state, do x = 0 and y = 0 then S1, is shorthand for do x = 0 and y = 0 until true then S1.
It is also possible to enter a state without resetting its internal memory (as in the entry-by-history of StateCharts) using the continue transitions. The modified example,
let node time_sharing c = (x, y) where rec automaton | Init -> do x = 0 and y = 0 continue S1 | S1 -> do x = 0 -> pre x + 1 until c continue S2 | S2 -> do y = 0 -> pre y + 1 until c continue S1 end
has the execution trace:
This is a way of writing activation conditions. It is convenient, for instance, for programming a scheduler which alternates between different computations, each of them having its own state.
It is possible to perform an action on a transition. As an example, consider programming a simple mouse controller with the following specification.
Return the event double whenever two clicks are received in less than four tops. Emit simple if only one click is received within the interval.
Here is one possible implementation:
let node counting e = cpt where rec cpt = if e then 1 -> pre cpt + 1 else 0 -> pre cpt
let node controller (click, top) = (simple, double) where rec automaton | Await -> do simple = false and double = false until click then One | One -> do until click then do simple = false and double = true in Await else (counting top = 4) then do simple = true and double = false in Await end
This program waits for the first occurrence of click, then it enters the One state and starts to count the number of tops. This state is exited when a second click occurs or when the condition counting top = 4 becomes true.
Note that the One state has two outgoing weak transitions (the second prefixed by else. As for the present construct, transition guards are evaluated in order from top to bottom. The first to be satisfied is triggered.
Any set of equations can be placed between the do/in of a transition, exactly as between a do/until or do/unless.
In the automata considered until now, the conditions on transitions have been boolean expressions. The language also provides a more general mechanism for testing signals and accessing their values on transitions.
Using signals, we can reprogram the mouse controller of the previous section as follows.
type event = Simple | Double let node controller (click, top) = o where automaton | Await -> do until click then One | One -> do until click then do emit o = Double in Await else (counting top = 4) then do emit o = Simple in Await end
This time no variables are defined in state Await. Writing emit o = x means that o is a signal and not a regular stream, there is thus no need to define it in every state of the automaton nor to declare a last value. The signal o is only emitted in state Emit. Otherwise, it is absent.
Combining signals with a sum type, as is done here, has some advantages over the use of boolean variables in the original program. By construction, only three values are possible for the output: o can only be Simple, Double or absent. In the previous version, a fourth case corresponding to the boolean value simple & double is possible, even though it is meaningless.
The signal patterns introduced in section 1.3.2 for the present construct may also be used in transition conditions to combine signals and access their values.
Consider, for example, the system below that has two input signals inc and dec, and that outputs a stream of integers o.
let node switch (inc, dec) = o where rec automaton | Init -> do o = 0 until inc(u) then Up(u) else dec(u) then Down(u) | Up(u) -> do o = last o + u until dec(v) then Down(v) | Down(v) -> do o = last o - v until inc(u) then Up(u) end
The condition until inc(u) means: await the presence of the signal low with some value u, then transition to the parameterized state Up(u).
A basic preemption condition has the form e(p) where e is an expression of type t sig and p is a pattern of type t. The condition binds the variables in the pattern p from the value of the signal at the instant when e is present. In the above example, for instance, the variable u is introduced and bound over the rest of the transition. A test for signal presence can be combined with a boolean condition. For example,
let node switch (inc, dec) = o where rec automaton | Init -> do o = 0 until inc(u) then Up(u) else dec(u) then Down(u) | Up(u) -> let rec timeout = 0 -> pre timeout + 1 in do o = last o + u until dec(v) & (timeout > 42) then Down(v) | Down(v) -> let rec timeout = 0 -> pre timeout + 1 in do o = last o - v until inc(u) & (timeout > 42) then Up(u) end
This system has the same behavior except that the presence of dec in the Up state is only taken into account when the timeout stream has passed the value 42.