Skip to main content
PRL Project

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:6The 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 ebe the most recent such X-event before e, {v} = ( SM1-class  init  (tr , X ))(e)

We can define7The definition we use for SM1-class is not literally this one, but is equivalent to it. these combinators as follows:

   class SM1-class init (tr,X) = tr o (X, Prior(self)?init) ;; 
   class Memory1 init tr X = Prior(SM1-class init (tr,X))?init ;;

Thus, if we declare

   class Y = SM1-class init (tr,X);; 
   class PrY = Memory1 init tr X;;

we know that that the following equations are satisfied:

   Y = tr o (X,Prior(Y)?init) 
   PrY = Prior(Y)?init

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:

  • Ai, a type of input values
  • S, a type representing values of the state
  • Xi : Class(Ai) recognizing input events
  • init : Loc Bag(S), assigning a bag of initial states to each location
  • tri : Loc Ai S S, assigning transition functions to each location

Together with init, each of the pairs tri,Xidefines a state machine with the same state type, S, but possibly different types of input values. In the idiomatic case, the X1-events and the X2-events are disjoint and the state machine we want to define acts as follows: If e is an Xi-event, it takes the transition defined by tri. (The definition will guarantee that if e should be both an X1-event and an X2-event, the state machine takes transition tr1.)

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