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 2²⁰ = 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.