1.4  Hierarchical State Machines

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 [9].

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.

1.4.1  Strong Preemption

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.

1.4.2  Weak Preemption

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)

---

Figure 1.3: Automata with weak (at left) and strong (at right) transitions

---

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.

1.4.3  Parameterized States

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

1.4.4  Modular Resets

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 ones⁵—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.

---

Figure 1.4: The ABRO automaton

---

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

1.4.5  Local State Definitions

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

1.4.6  States and Shared Memory

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 [16], 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

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.

1.4.7  The Initial State

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

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:

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, r) = o where
  rec automaton
      | Run(incr) ->
          do o = 0 fby o + incr until idle() then Idle
      | Idle ->
          do until r(incr) then Run(incr)
      init Run(i0)

1.4.8  Resuming a State

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.

1.4.9  Actions on Transitions

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.

1.4.10  Signals and State Machines

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.

1.4.11  Pattern Matching over Signals

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.

5

As in OCaml, identifiers starting with an uppercase letter are considered to be data type constructors and cannot be used as variable names.