Synchronizing events

The power of events is that they synchronize. To illustrate this, consider the following CIF specification:

automaton producer:
  event produce, provide;

  location producing:
    initial;
    edge produce goto idle;

  location idle:
    edge provide goto producing;
end

The automaton represents a producer that produces products, to be consumed by a consumer. The producer automaton starts in its producing location, in which it produces a product. Once the product has been produced, indicated by the produce event, the automaton will be in its idle location, where it waits until it can provide the produced product to the consumer. Once it has provided the product to the consumer, it will once again be producing another product. Consider also the following continuation of the above specification:

automaton consumer:
  event consume;

  location idle:
    initial;
    edge producer.provide goto consuming;

  location consuming:
    edge consume goto idle;
end

This second automaton represents a consumer that consumes products. The consumer is initially idle, waiting for a product from the producer. Once the producer has provided a product, the consumer will be consuming. Once it has consumed the product, as indicated by the occurrence of the consume event, it will become idle again.

The specification has three events, the produce and provide events declared in the producer automaton, and the consume event declared in the consumer automaton. The consumer automaton, in its idle location, has an edge that refers to the provide event declared in the producer automaton. As such, that edge and the edge in the idle location of the producer automaton, refer to the same event.

Synchronization

Events that are used in multiple automata, must synchronize. That is, if one of those automata performs a transition for that event, the other automata must also participate by performing a transition for that same event. If one of the automata that uses the event can not perform a transition in its current location, none of the automata can perform a transition for that event.

Now, lets take a closer look at the behavior of the producer/consumer example. Initially, the producer automaton is in its producing location, and the consumer automaton is in its idle location. Since the producer is the only automaton that uses the produce event, and there is an (outgoing) edge in its current location for that produce event, the producer can go to its idle location by means of that event.

Both the producer and consumer use the provide event. The producer has no edge with that event in its producing location, while the consumer does have an edge for that event in its idle location. Since events must synchronize, and the producer can not participate, the event can not occur at this time. This is what we expect, as the producer has not yet produced a product, and can thus not yet provide it to the consumer. The consumer will have to remain idle until the producer has produced a product and is ready to provide it to the consumer.

The producer blocks the provide event in this case, and is said to disable the event. The event is not blocked by the consumer, and is thus said to be enabled in the consumer automaton. In the entire specification, the event is disabled as well, as it is disabled by at least one of the automata of the specification, and all automata must enable the event for it to become enabled in the specification.

The only behavior that is possible, is for the producer to produce a product, and go to its idle location. The consumer does not participate and remains in its idle location. Both automata are then in their idle location, and both have an edge that enables the provide event. As such, the provide event is enabled in the specification. As this is the only possible behavior, a transition for the provide event is performed. This results in the producer going back to its producing location, while at the same time the consumer goes to its consuming location.

In its producing location, the producer can produce a product. Furthermore, in its consuming location, the consumer can consume a product. Two transitions are possible, and CIF does not define which one will be performed. That is, either one can be performed. No assumptions should be made either way. In other words, both transitions represent valid behavior, as described by this specification. Since only one transition can be taken at a time, there are two possibilities. Either the producer starts to produce the product first, and the consumer starts to consume after that, or the other way around.

Traces and state spaces

Once both transitions have been taken, we are essentially in the same situation as we were after the producer produced a product the first time, as both automata will be in their idle locations again. The behavior of the specification then continues to repeat forever. However, for each repetition different choices in the order of production and consumption can be made.

During a single execution or simulation, choices are made each time that multiple transitions are possible. The sequence of transitions that are taken is called a trace. Examples of traces for the producer/consumer example are:

  • produce → provide → produce → consume → provide → produce → consume → …​

  • produce → provide → produce → consume → provide → consume → produce → …​

  • produce → provide → consume → produce → provide → produce → consume → …​

  • produce → provide → consume → produce → provide → consume → produce → …​

The traces end with ... to indicate that they are partial traces, that go beyond the part of the trace that is shown. These four traces however, cover all the possibilities for the first seven transitions.

All possible traces together form the state space, which represents all the possible behavior of a system. For the producer/consumer example, the state space is:

producer consumer state space finite

Here the circles represent the states of the specification, which are a combination of the states of the two automata. The labels of the circles indicate the state, as a combination of the first letters of the locations of the automata. The initial state is labeled p/i, as initially automaton producer is in its producing (p) location, and the consumer is in its idle (i) location. The arrows indicate the transitions, and are labeled with events. The state space clearly shows the choices, as multiple outgoing arrows for a single state. It also makes it clear that as we move to the right, and make choices, we can make different choices for different products. Since the behavior keeps repeating itself, the state space ends with ... to indicate that only a part of the state space is shown.

However, we can also show the entire behavior of the specification. Essential here is that the state space shown above has duplicate states. That is, several states have the same label, and allow for the same future behavior. By reusing states, a finite representation of the state space can be made, which shows the entire possible infinite behavior of the producer/consumer specification:

producer consumer state space infinite

Concluding remarks

By using multiple automata, the producer and consumer were modeled independently, allowing for separation of concerns. This is an important concept, especially when modeling larger systems. In general, the large system is decomposed into parts, usually corresponding to physical entities. Each of the parts of the system can then be modeled in isolation, with little regard for the other parts.

By using synchronizing events, the different automata that model different parts of a system, can interact. This allows for modeling of the connection between the different parts of the system, ensuring that together they represent the behavior of the entire system.