## 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:

 x false false true false false true … expect x false false true true true true …

### 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
```
 x false false true false false true … expect x false false false true true true …

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.

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

```(* 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:

 i 0 0 0 0 0 0 0 0 0 0 0 0 … min 0 0 0 0 0 0 0 0 0 -1 0 0 … max 4 4 4 4 4 4 4 4 4 4 4 4 … last o 0 1 2 3 4 3 2 1 0 -1 0 1 … o 1 2 3 4 3 2 1 0 -1 0 1 2 … last o + 1 1 2 3 4 0 1 2 … last o - 1 3 2 1 0 -1 …

### 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
```
 i 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 … min 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 … max 0 0 0 4 4 4 4 4 4 4 4 4 4 4 4 … last o 0 0 0 0 1 2 3 4 3 2 1 0 -1 0 1 … o 0 0 0 1 2 3 4 3 2 1 0 -1 0 1 2 … last o + 1 0 0 0 1 2 3 4 0 1 2 … last o - 1 0 0 0 3 2 1 0 -1 …

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:

 i 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 … min 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 … max 0 0 0 4 4 4 4 4 4 4 4 4 4 4 4 … last o 0 0 0 0 1 2 3 4 3 2 1 0 -1 0 1 … o 0 0 0 1 2 3 4 3 2 1 0 -1 0 1 2 … last o + 1 0 0 0 1 2 3 4 0 1 2 … last o - 1 0 0 0 3 2 1 0 -1 …

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
```
 min 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 … max 0 0 0 4 4 4 4 4 4 4 4 4 4 4 4 … o 0 -1 0 1 2 3 4 3 2 1 0 -1 0 1 2 …

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.