//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[lang-tut-basics-chapter-synchronizing-events]]
== Synchronizing events

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

// Copied to: basics/alphabet
// Copied to: basics/event-placement
// State space in lesson: extensions/annotations
[source, cif]
----
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:

// Copied to: basics/alphabet
// Copied to: basics/event-placement
[source, cif]
----
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.

indexterm:[synchronization]

=== 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`.

[[lang-tut-basics-chapter-synchronizing-events-enabled]]
indexterm:[event,enabled]
indexterm:[event,disabled]
indexterm:[event,enabledness]
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.

[[lang-tut-basics-chapter-synchronizing-events-trace]]
indexterm:[execution simulation trace]
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.

[[lang-tut-basics-chapter-synchronizing-events-statespace]]
indexterm:[state space]
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:

image::{lang-tut-imgsdir}/basics/producer_consumer_state_space_finite.png[]

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:

image::{lang-tut-imgsdir}/basics/producer_consumer_state_space_infinite.png[]

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