1.7  Parameterized State Machines

In the examples we have considered so far, an automaton is made of a finite set of states and transitions. It is possible to define more general state machines containing parameterized states, that is, states that may be initialized with some input values. Parameterized states are a natural way to pass informations from states to states and to reduce the number of states. A full section is dedicated to automata with parameterized states because as they lead to a different style of programming.

The following program is a simple counter that counts the number of occurrences of x:

let node count 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

This automaton simulates an infinite state machine with states Zero, Plus(1), Plus(2), etc.

We now come back to the example of the mouse controller whose informal specification is reminded below:

Return the event double when two click has been received in less than four top. Emits simple if only one click has been received.

This specification is too informal and says nothing about the precise instant where double or simple must be emitted. The mouse controller can be programmed as a three states automaton:

let node counting e = cpt where
  rec cpt = if e then 1 -> pre cpt + 1 else 0 -> pre cpt

let node controler click top = (simple, double) where
  automaton
    Await ->
     do  simple = false and double = false
     until click then One
  | One ->
     do  simple = false and double = false
     unless click then Emit(false, true)
     unless (counting top = 4) then Emit(true, false)
  | Emit(x1, x2) ->
     do simple = x1 and double = x2
     until true then Await
  end

It first awaits for the first occurrence of click, then it enters in state One, starting to count the number of top. This state can be preempted strongly when a second click occurs or that the condition counting top = 4 is true. For example when click is true, the control immediately enters in state Emit(false, true), giving the initial values false to x1 and true to x2. Thus, at the same instant, simple = false and double = true. Then, the control goes to the initial state Await at the next instant.

This example illustrates an important feature of automata in Lucid Synchrone: only one set of equations is active during a reaction but it is possible to compose (at most) one strong preemption followed by a weak preemption during on reaction. This is precisely what we made in the previous example. As opposed to other formalisms (e.g., StateCharts) it is impossible to cross an arbitrary number of states during a reaction.