### 4 State machines

Previous examples have built state machine classes by hand, from EventML primitives. The Nuprl library defines combinators that package up idioms for defining state machines of various kinds. Many of the automated tactics created to reason about event classes are tuned for definitions that use these combinators.

#### 4.1 Moore machines, “pre” and “post”

We have been using a standard strategy. First define what might loosely be called a Moore machine: in response to inputs it updates its state and makes that state visible. We then use the simple composition combinator to define a Mealy machine (loosely called) from this Moore machine: one that, in response to some of the Moore machine’s inputs, returns directed messages. One virtue of this factoring is that, by making the state visible, we can conveniently express state invariants as properties of classes explicitly defined in the EventML code.

In general, we can define a Moore machine from the following data:

- A, the type of input values
- S, the type of state values
- X : Class(A), recognizing input events
- init : Loc → Bag(S), assigning a bag of initial states to each location
- tr : Loc → A → S → S, assigning a transition function to each location

We introduce combinators, SM1-class and Memory1, that provide two different ways to observe this state machine. In the idiomatic case, in which init assigns a singleton bag to every location:

- ( SM1-class init (tr , X )) is the “post” observer of the state machine, which behaves as follows:
- The events it recognizes are the X-events.
- To every X-event e it assigns a singleton bag {v}, where v is the state of that state machine after responding to e.

- ( Memory1 init tr X ) is the “pre” observer of the state machine, which behaves as
follows:
^{6}The use of two separate parameters, tr and X, rather than a single pair, is a slightly awkward bit of legacy that will eventually be changed.- It recognizes all events.
- To every event e it assigns a singleton bag, {v} where, intuitively, v is the value of the state
when e arrives (before it is processed).
More precisely, if there has been no previous X-event at location loc(e), {v} = (init loc(e)); otherwise, letting e′ be the most recent such X-event before e, {v} = ( SM1-class init (tr , X ))(e′)

We can define^{7}The definition we use for SM1-class is not literally this one, but is equivalent to it.
these combinators as follows:

Thus, if we declare

we know that that the following equations are satisfied:

#### 4.2 Moore machines with multiple transition functions

One often wants a state machine whose inputs are defined by two or more different classes—typically, base classes that recognize inputs of different kinds. For notational simplicity, consider the case of two input classes. Now we have, for i = 1,2:

- A
_{i}, a type of input values - S, a type representing values of the state
- X
_{i}: Class(A_{i}) recognizing input events - init : Loc → Bag(S), assigning a bag of initial states to each location
- tr
_{i}: Loc → A_{i}→ S → S, assigning transition functions to each location

Together with init, each of the pairs ⟨tr_{i},X_{i}⟩ defines a state machine with the same state type, S, but
possibly different types of input values. In the idiomatic case, the X_{1}-events and the X_{2}-events are disjoint and
the state machine we want to define acts as follows: If e is an X_{i}-event, it takes the transition defined by tr_{i}.
(The definition will guarantee that if e should be both an X_{1}-event and an X_{2}-event, the state machine takes
transition tr_{1}.)

As before, we can define classes that represent both “post” and “pre” observations of this state machine (for the idiomatic case):

- ( SM2-class init (tr
_{1 }, X_{1 }) (tr_{2 }, X_{2 })) is the “post” observer. The events it recognizes are X_{1 }-events or X_{2}-events. - ( Memory2 init tr
_{1 }X_{1 }tr_{2 }X_{2 }) is the “pre” observer, which recognizes all events.

SM3-class/Memory3 and SM4-class/Memory4 are similar, except that they combine, respectively, three and four different sources of inputs.

Note: EventML is rich enough to define all of these classes. For technical reasons, their official definitions use features of the Nuprl type system not available in EventML, so we prefer simply to make instances of these combinators available as quasi-primitives.