1.6  State Machines

The language provides means to define state machines, as a way to describe directly control dominated systems. These state machines can be composed in parallel with regular equations or other state machines and can be arbitrarily nested.

In this tutorial, we first consider state machines where transitions are only made of boolean expressions. Then, we consider two important extensions of the basic model. The first one is the ability to build define state machines with parameterized states. The second one introduces the general form of transitions made of signal matching and boolean expressions.

An automaton is a collection of states and transitions. A state is made of a set of equations in the spirit of the Mode-automata by Maraninchi & Rémond. Two kinds of transitions are provided, namely weak and strong transitions and for each of them, it is possible to enter in the next state by reset or by history. One important feature of these state machines is that only one set of equations is executed during one reaction.

1.6.1  Strong Preemption

Here is a two state automaton illustrating strong preemption. The function expect awaits x to be true and emits true for the remaining instants.

(* await x to be true and then sustain the value *)
let node expect x = o where 
  automaton
    S1 -> do o = false unless x then S2
  | S2 -> do o = true done
  end

val expect :  bool => bool
val expect :: ’a -> ’a

This automaton is made of two states, each of them defining the value of a shared variable o. The keyword unless indicates that o is defined by the equation o = false from state S1 while x is false. At the instant where x is true, S2 becomes the active state for the remaining instant. Thus, the following chronogram hold:

1.6.2  Weak Preemption

On the contrary, the following function emits false at the instant where x is true and true for the remaining instants, thus corresponding to regular Moore automata.

(* await x to be true and then sustain the value *)
let node expect x = o where 
  automaton
    S1 -> do o = false until x then S2
  | S2 -> do o = true done
  end

val expect :  bool => bool
val expect :: ’a -> ’a

The classical two states switch automaton can be written like the following:

let node weak_switch on_off = o where
  automaton
    False -> do o = false until on_off then True
  | True -> do o = true until on_off then False
  end

Note the difference with the following form with weak transitions only:

let node strong_switch on_off = o where
  automaton
    False -> do o = false unless on_off then True
  | True -> do o = true unless on_off then False
  end

We can check that for any boolean stream on_off, the following property holds:

weak_switch on_off = strong_switch (false -> pre on_off)

The graphical representation of these two automata is given in figure 1.5.

---

Figure 1.5: Two automata with strong and weak transitions

---

Weak and strong conditions can be arbitrarily mixed as in the following variation of the switch automaton:

let node switch2 on_off stop = o where
  automaton
    False -> do o = false until on_off then True
  | True -> do o = true until on_off then False unless stop then Stop
  | Stop -> do o = true done
  end

Compared to the previous version, state True can be strongly preempted when some stop condition stop is true.

1.6.3  ABRO and Modular Reseting

The ABRO example is due to Gérard Berry [2]. It highlight the expressive power of parallel composition and preemption in Esterel. The specification is the following:

Awaits the presence of events A and B and emit O at the exact instant where both events have been received. Reset this behavior every time R is received.

Here is how we write it, replacing capital letters by small letter ⁷.

(* emit o and sustain it when a and b has been received *)
let node abo a b = (expect a) & (expect b)

(* here is ABRO: the same except that we reset the behavior *)
(* when r is true *)
let node abro a b r = o where
  automaton
    S1 -> do o = abo a b unless r then S1
  end

The node abro is a one state automaton which resets the computation of abo a b: every stream in abo a b restarts with its initial value. The language provides a specific reset/every primitive as a shortcut of such a one-state automaton and we can write:

let node abro a b r = o where
  reset
    o = abo a b
  every r

The reset/every construction combines a set of parallel equations (separated with an and). Note that the reset operation correspond to strong preemption: the body is reseted at the instant where the condition is true. The language does not provide a “weak reset”. Nonetheless, it can be easily obtained by inserting a delay as illustrated below.

  let node abro a b r = o where
    reset
      o = abo a b
    every true -> pre r

1.6.4  Local Definitions in a State

It is possible to define names which are local to a state. These names can only be used inside the body of the state and may be used in weak conditions only.

The following programs integrates the integer sequence v and emits false until the sum has reached some value max. Then, it emits true during n instants.

let node consumme 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 which can be used to compute the weak condition c = max and this does not introduce any causality problem. Indeed, weak transitions are only effective during the next reaction, that is, 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 counting v = cpt where
  rec cpt = v -> pre cpt + v

let node consumme max n v = status where
  automaton
    S1 ->
       do status = false
       until (counting v = max) then S2
  | S2 ->
       do status = true
       until (counting 1 = n) then S1
  end

The body of a state is a sequence (possibly empty) of local definitions (with let/in) followed by some definitions of shared names (with do/until). As said previously, weak conditions may depend on local names and shared names.

It is important to notice that using unless instead of until leads to a causality error. Indeed, in a strong preemption, the condition is evaluated before the equations of the body and thus, cannot depend on them. In a weak preemption, the condition is evaluated at the end, after the definitions of the body have been evaluated. Thus, when writting:

let node consumme 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 + v in
      do status = true
      unless (c = n) then S1
  end

The compiler emits the message:

File "tutorial.ls", line 6:
> unless c = max then S2
>        ^^^^^^^
This expression may depend on itself.

1.6.5  Communication between States and Shared Memory

In the previous examples, there is no communication between values computed in each state. Consider a simple system made of two running modes as seen previously. In the Up mode, the system increases some value with a fixed step 1 whereas in the Down mode, this value decreased with the same step. Now, the transition from one mode to the other is described by a two-state automaton whose behavior depends on the value computed in each mode. This example, due to Maraninchi & Rémond [8] can be programmed in the following way.

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 last o = i

An execution diagram is given below:

1.6.6  The Particular Role of the Initial State

The initial state can be used for defining some variables whose value can then be sustained in remaining states. In that case, their last value is considered to be defined. Moreover, it becomes possible not to define their value in all the 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

Because 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. Note that replacing the weak preemption by a strong one will lead to 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
          until (o = max) then Down
      | Down -> 
          do o = last o - 1
          until (o = min) then Up
      end

and we get:

File "tutorial.ls", line 128, characters 20-30:
>                o = last o + 1
>                    ^^^^^^^^^^
This expression may not be initialised.

We said previously that strong conditions must not depend on some variables computed in the current state but they can depend on some shared memory last o as in:

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
          unless (last o = max) then Down
      | Down -> 
          do o = last o - 1
          unless (last o = min) then Up
      end

and we get the same execution diagram as before:

Note that the escape condition do x = 0 and y = 0 then Up in the initial state is a shortcut for do x = 0 and y = 0 until true then Up.

Finally, o do not have to be defined in all the states. In that case, it keeps its previous value, that is, an equation o = last o is implicitely added.

1.6.7  Resume a Local State

By default, when entering in a state, every computation in the state is reseted. We also provides some means to resume the internal memory of a state (this is called enter by history in UML diagrams).

let node two_modes min max = o where
  rec automaton
        Up -> do o = 0 -> last o + 1 until (o >= max) continue Down
      | Down -> do o = last o - 1 until (o <= min) continue Up
      end

This is an other way to write activation conditions and is very convenient for programming a scheduler which alternate between some computations, each of them keeping its own state as in:

let node time_sharing c i = (x,y) where
  rec automaton
        Init ->
          do x = 0 and y = 0 then S1
      | S1 ->
          do x = 0 -> pre x + 1 until c continue S2
      | S2 ->
          do y = 0 -> pre y + 1 until c continue S1
      end

7

As in Objective Caml, identifiers starting with a capital letter are considered to be constructors and cannot be used for variables.