Version:
v9.0-RC1
[release notes]

# Module 2.3: Synchronizing automata

Larger systems consist of sub-systems and sub-sub-systems, with various components. In Module 1, you already learned to model each component separately as an automaton. This way, you model several smaller automata, rather than a much larger single automaton.

For instance, consider a system consisting of 20 independent conveyer belts. Let say, to keep it simple, that each belt has only two states, as it can be on or off. Since the state of the system is the combined state of each of its parts, the system would then have 220 = 1,048,576 states. Clearly, modeling each state separately is not feasible. Using a collection of automata, which is sometimes also called a network of automata, is then more convenient. Then each conveyer belt can be modeled with just two locations, for a total of 40 locations in total.

So far, if you used multiple automata, each automaton had its own events, and thus operated independently of the other automata. In this sub-module you learn about synchronizing automata, that use each others events and thereby interact with each other. Synchronization is a key concept of the CIF modeling language.

## Synchronization on events

The power of events is that they synchronize. That is, when multiple automata have an event in their alphabet, a transition for that event can only occur if these automata can all participate at the same time. If only one of them does not have an enabled edge for the event, a transition is not possible for the event. Thus if one of them does not have an edge for the event in its current location, or it does have an edge but its guard condition is not satisfied, then none of the other automata can take an edge for the event either. If all automata that should participate do have an enabled edge for the event, a transition is possible for the event, and all automata take an edge at the same time. They thus synchronize, either all together taking a step, or not at all. If an automaton can take an edge for an event, it is said to enable the event. Only if all automata in the system that have the event in their alphabet enable the event, then they can together take a transition for the event. If an automaton can not take any edge for an event, and this event is in its alphabet, then it is said to block or disable the event. If only just one automaton blocks an event, no transition for that event can occur in the entire system. An automata that does not have a certain event in its alphabet, does not participate in transitions for that event, and also does not block it.

As an example, consider a driver of a car that can break down, and a mechanic that can repair the car. We can model their interactions using the following two automata, where the top automaton models the driver and the bottom automaton the mechanic:

The driver is initially driving the car (location `Driving`). Once the car breaks down (event `breakdown`), the driver prepares to call the mechanic (location `PreparingToCall`). After calling the mechanic (event `call_mechanic`), the driver waits for the repairs to be completed (location `Waiting`). Once the repairs have been completed (event `repair_finished`), and the car is again in working order, the driver can continue driving it (location `Driving`). If the car breaks down again, the driver will again call the mechanic, and so on.

The mechanic is initially not working (location `NotWorking`). Once a call comes in from the driver (event `call_mechanic`), the mechanic prepares to start repairs on the car (location `PreparingToRepair`). After the preparations, the mechanic starts repairing the car (event `start_repair`), which takes some time (location `Repairing`). Once the repairs have been completed (event `repair_finished`), the mechanic is done and is no longer working on the car (location `NotWorking`). Should another call come in, the mechanic will again repair the car, and so on.

The driver's automaton uses three events: `breakdown`, `call_mechanic` and `repair_finished`. The mechanic's automaton also uses three events: `call_mechanic`, `start_repair` and `repair_finished`. The `call_mechanic` and `repair_finished` events are used by both automata (they share the events), while the `breakdown` event is used only by the driver, and the `start_repair` event only by the mechanic.

Now consider the combined behavior of the driver and the mechanic, taking into account their interactions. Initially, the driver is driving (location `Driving`), and the mechanic is not working (location `NotWorking`). The mechanic is waiting for a call, but it won't come in at this time, since the driver will only call in its `PreparingToCall` location. Since the driver has no edge for the `call_mechanic` event in its current location (`Driving`), the event is not enabled. The mechanic thus continues to wait for the call. The driver will keep driving until the car breaks down (event `breakdown`). Since only the driver automaton uses this event, no other automaton needs to synchronize. Once the car breaks down, the driver automaton will go its `PreparingToCall` location. Then the driver will call the mechanic (event `call_mechanic`). This involves an interaction between the driver and the mechanic. After this event, the driver will go to its `Waiting` location, and the mechanic will go its `PreparingToRepair` location. The driver has to wait for the repair to have finished (event `repair_finished`), which can not occur yet, as the mechanic has not started the repair, let alone finished it. That is, the driver has an outgoing edge for the `repair_finished` event in its current location, but the mechanic does not. The mechanic can however start the repair (event `start_repair`) and go its `Repairing` location. Once the mechanic then finishes the repair (event `repair_finished`), the driver can go back to `Driving` and the mechanic is again `NotWorking`. This is again a synchronization, so both automata go to their next locations simultaneously.

## Event placement

When multiple automata use an event, and synchronize on it, the event is only declared once. This begs the question where the declaration of the event should be placed in a CIF model.

In many cases it is clear in which automaton the event should be declared. For instance, the event for the car breaking down belongs logically with the driver of the car, as that automaton is the only automaton that uses the event. And the mechanic being finished with repairing the care belongs logically with the mechanic, as the mechanic performs the action. The driver synchronizes on the event of the mechanic being done, and reacts to it, but does not perform the action.

There are however events for which it is more difficult to determine in which automaton to declare them. For instance, the event to call the mechanic involves both the driver and the mechanic. One could argue that the driver initiates the action, and thus the event should be declared in the driver's automaton. But, one could also argue that the mechanic is being called, and thus the event should be declared in the mechanic's automaton. In cases where it is less clear in which automaton to declare the event, there is another option: declare the event outside the automata.

In general, it is best to place events as close as possible to where they are used (initiated, executed, and so on). As an example, consider the following CIF model of the driver and mechanic, with some events declared in the automata, and some outside the automata.

                                event call_mechanic;

                                automaton Driver:
                                    event breakdown;

                                    location Driving:
                                        initial;
                                        marked;
                                        edge breakdown goto PreparingToCall;

                                    location PreparingToCall:
                                        edge call_mechanic goto Waiting;

                                    location Waiting:
                                        edge Mechanic.repair_finished goto Driving;
                                end

                                automaton Mechanic:
                                    event start_repair, repair_finished;

                                    location NotWorking:
                                        initial;
                                        marked;
                                        edge call_mechanic goto PreparingToRepair;

                                    location PreparingToRepair:
                                        edge start_repair goto Repairing;

                                    location Repairing:
                                        edge repair_finished goto NotWorking;
                                end

Events declared in the same automaton as where they are used (on edges), can be referred to only by their name. Similarly, events declared outside the automata can also be referred to directly by their name. Events declared in other automata, on the other hand, have are to prefixed with the name of that automaton and a period, such as `Mechanic.repair_finished` in the example above.

## Quiz

Consider the following two automata for the first five questions.

[ { type: 'multiple-choice', question: "What are the shared events of the two automata?", answers: [ "Event `a`.", "Event `b`.", "Event `c`.", "Event `d`.", "Event `e`.", "Event `f`." ], correctAnswer: '2, 3' }, { type: 'multiple-choice', question: "For which events can transitions happen when the top automaton is in location `2` and the bottom one is in location `1`?", answers: [ "Event `a`.", "Event `b`.", "Event `c`.", "Event `d`.", "Event `e`.", "Event `f`." ], correctAnswer: '2, 4, 6' }, { type: 'multiple-choice', question: "For which events can transitions happen when both automata are in location `1`?", answers: [ "Event `a`.", "Event `b`.", "Event `c`.", "Event `d`.", "Event `e`.", "Event `f`." ], correctAnswer: '3, 5' }, { type: 'single-choice', question: "When considering only the top automaton, and assuming it is the only automaton in a model, does it then have deadlock?", answers: [ "Yes, from location `3` the automaton cannot go back to locations `1` and `2`.", "Yes, in location `3` there is no behavior possible.", "No, there is no situation in which no further behavior is possible." ], correctAnswer: '3' }, { type: 'single-choice', question: "When considering only the top automaton, and assuming it is the only automaton in a model, is it blocking?", answers: [ "Yes, once in location `3` the automaton cannot go to a marked location.", "No, all its locations are reachable from its initial location." ], correctAnswer: '1' }, { type: 'single-choice', question: ` What would happen with the behavior of the driver and the mechanic, if the driver would have location `Waiting` as its initial location instead of location `Driving`? Select the best answer.`, answers: [ "This does not matter, as the change only affects the initial state, and the two automata are still deadlock-free and non-blocking.", "The individual automata still do not have deadlock, but the entire system now does. No further behavior is possible right from the start.", "The automata then do not correctly model the behavior of the interactions between the driver and the mechanic." ], correctAnswer: '2' }, { type: 'single-choice', question: ` Let's say you have to model a button that can be pushed and released, and a motor that can be turned on and off. Pushing the button turns on the motor, and pushing it again turns off the motor. Where would you place the events of the button being pushed and released? Select the best answer.`, answers: [ "Either in the button automaton, the motor automaton, or outside the automata. It does not matter.", "In the automaton of the button, since it is the button that is pushed and released.", "In the automaton of the motor, because pushing and releasing the button directly affects the motor.", "Outside the automata, since the button and motor interact and it is therefore difficult to decide a specific automaton to declare the events." ], correctAnswer: '2' } ]