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.
Here is a two state automaton illustrating strong preemption. The
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
o is defined by the equation
o = false
x is false. At the instant where
x is true,
S2 becomes the active state for the remaining
instant. Thus, the following chronogram hold:
On the contrary, the following function emits
false at the
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
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
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.
The ABRO example is due to Gérard Berry . It highlight the expressive power of parallel composition and preemption in Esterel. The specification is the following:
Awaits the presence of events
Oat the exact instant where both events have been received. Reset this behavior every time
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
abro is a one state automaton which resets the
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
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
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
emits false until the sum has reached some value
max. Then, it
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
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
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
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.
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
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  can be programmed in the
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:
|last o + 1||1||2||3||4||0||1||2||…|
|last o - 1||3||2||1||0||-1||…|
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
|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
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
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:
|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.
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.
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