Example 1. StateMachine

A FORMULA domain contains a collection of type declarations, rules, and conformance constraints. Here is a basic FORMULA domain describing a class of state machines.

domain StateMachine
{
    Event ::= new (name: String, lbl: Integer).
    States ::= new (name: String, lbl: {Initial, Regular, Final}).
    Transition ::= new (current: States, target: States, guard: Event).

    conforms count({ i | i is States(_, Initial) }) = 1.
    conforms count({ f | f is States(_, Final) }) >= 1.
}

To define a class of state machines is to create a representation for state machines using FORMULA data types. A state machine can be represented by its states, the transitions between different states, and the events which guard the transitions. So the first three lines in the above domain module are the declarations of data constructors Event, States and Transitions. The left-hand side of the declaration is the name of the constructor and the right-hand side is a comma-separated list of argument types with parenthesis. Every constructor must have at least one argument, otherwise it would be constant.

Next we take a look at the conformance constraints on the bottom two lines. To create a conformance constraint we use the syntax

conforms body.

For a state machine to conform to its domain, it has to satisfy all the conformance constraints for some substitution of the variables. Thus the state machines of this domain must have exactly one initial state and at least one final states.

Though these constructors and constraints provide representations and constraints of a state machine, the domain does not define any specific state machine. This is because the domain is intended as a schema for all state machines; it is not intended to represent a specific state machine. A specific state machine is represented by a model, as follows:

model Server of StateMachine
{
    e is Event("Right info received", 1).
    init is States("Wait for request", Initial).
    fn is States("Info sent", Final).

    Transition(init, fn, e).
}

A model has a name and indicates the domain to which it belongs, so in this example, our model has name “Server” and it belongs to the domain StateMachine which we just created. The body of a model contains a list of values separated by periods, Event("Right info received", 1), States("Wait for request", Initial), States(“Info sent", Final) and Transition(init, fn, e). It indicates that this model machine is initially in the state “Wait for request”, and goes through the transition to the final state “Info sent” guarded by the event “Right info received”. These periods are actually assertions about the model, indicating "The value f (. . .) is always provable in the model Server.” Thus, the model Server contains a set of assertions, built with data constructors, about some events, states and transitions. These assertions define the specific elements of the state machine.

Now since the values may be reused in many places, aliases are introduced with special syntax is. The right-hand side of the is keyword requires a constructed assertion. The left-hand side is an identifier that stands for the constructed value. Aliases can be used to represent models with exponentially less space. As in the model Server, in order to describe a transition from the initial state “Wait for request” to the final state “info sent” guarded by the event “Right info sent”, we just use the aliases e, init and fn instead of squeezing the three long data with arguments into the Transition data constructor.