Module 3.4: Modeling larger systems

So far, in the course, you've seen examples of systems that contain multiple similar automata. CIF features automaton definitions, a kind of parameterized templates that can be instantiated many times, making it easier to model multiple slightly different automata. And you've also seen larger systems, with many automata. For such systems, CIF features groups that add structure to model and allow you to keep a better overview. And CIF also features imports that make it possible to split your model over multiple files, allowing you to reuse parts of your models in other models.

Automaton definitions

When modeling large systems, your models may have many similar components or parts modeled as similar automata. For example, the model of the water lock in Module 2, included many sensors modeled as similar automata. And when, for instance, a conveyer belt system handling luggage at an airport consists of 20 conveyor belts, it would be cumbersome and time-consuming to copy the same automaton repeatedly. It can also hinder evolution of the model, as a change to one of the automata usually needs to be applied to the others as well. Therefore, CIF has automaton definitions acting as some sort of template that can be used multiple times. That is, automaton definitions are specified once and can be instantiated multiple times. Each automaton instantiation is then a concrete automaton, a copy of its definition.

As an example, consider again the hay baler and bale loader from the solution to Exercise 7a of Module 2. The baler1 and baler2 automata are exactly the same, except for the names of the automata. We can make an automaton definition that represents the behavior of a baler, and instantiate it twice, one for each baler:

                        
                            automaton def Baler():
                                event make_bale;
                                disc int bales = 0;

                                location:
                                    initial;
                                    marked;
                                    edge make_bale do bales := bales + 1;
                            end

                            baler1: Baler();
                            baler2: Baler();
                        
                    

The Baler automaton definition is nearly identical to the original baler1 and baler2 automata. The automaton definition is identified by the def keyword between the automaton keyword and the name of the automaton definition, as well as by the parentheses after its name.

An automaton definition by itself is not an automaton. The instantiations of the automaton definition, baler1 and baler2 in this case, however, are automata. Before the colon, the name of the instantiation is given, which indicates the name of the automaton that is produced by instantiating the automaton definition. After the colon, the name of the automaton definition that is to be instantiated is given. The above automaton definition and two instantiations baler1 and baler2, have the exact same behavior as the two original baler1 and baler2 automata.

Using automaton definitions and multiple instantiations, much of the duplication in a model can be avoided. This saves time and thereby improves modeling efficiency, as the duplicate parts don't each have to be written separately or be copied and adapted. Furthermore, it is easier to extend the model. If, for example, the neighboring farm decides to lend you their baler, the model can be easily extended by adding an extra automaton instantiation, which requires only one new line: baler3: Baler();. And making adaptations in a consistent way is also made easier, as when an automaton definition is adapted, all its instantiations are automatically and consistently adapted as well. For example, when changing the name of the bales variable to bales_made, the variable name only needs to be changed in the automaton definition. The automaton instantiations automatically adopt this change. Automaton definitions and instantiations thus allow for scalability and reuse and improve maintainability.

Similar to how an automaton can be labeled a plant, so too can automaton definitions. If a plant automaton definition is defined, and it is instantiated, then each instantiation is a plant automaton. That is, instead of automaton def Baler(): you could also write plant def Baler():.

In CIF, as a convention, names of automaton definitions usually start with an uppercase letter, while instantiations are usually given a name that start with a lowercase letter, just like automata. For instance, an automaton definition could be named LockDoor and the instantiations could be named left_door and right_door.

Parameterized automaton definitions

In practice, models often have similar, but not exactly identical automata. They are largely the same, but they differ in a few details. For instance, they could have the same variables, but with different values. Or they could have the same edges, but for different events. To support this, automaton definitions can be given parameters. And the instantiations can then give different arguments for these parameters.

Algebraic parameters

For instance, for the hay baler an bale loader example of Module 2, you also made a version of the bale loader that has a capacity of 10 bales, as part of Exercise 7b. Now consider that the farmer were to call a neighbor, who owns a bale loader with a capacity of 20 bales, to come help him. Both bale loader automata would be identical, except for the value of the load_capacity constant. With the parameterized automaton definition, it is still possible to make a template once and use it twice:

                        
                            automaton def BaleLoader(alg int load_capacity):
                                event load_bales;
                                disc int loaded_bales = 0;

                                alg bool enough_bales = bales_on_field >= load_capacity;

                                location:
                                    initial;
                                    marked;
                                    edge load_bales  when enough_bales do loaded_bales := loaded_bales + load_capacity;
                                    edge stop_baling when enough_bales;
                            end

                            baler_loader_small: BaleLoader(10);
                            baler_loader_large: BaleLoader(20);
                        
                    

The load_capacity constant has been replaced by a parameter. This parameter has the same name and type as the constant, but since it is a parameter it can be given different values for each instantiation. Automaton instantiation bale_loader_small provides value 10 and therefore represents the bale loader of the farmer. Automaton instantiation bale_loader_large provides value 20 and thus represents the neighbor's bale loader.

In this case, since a value is to be passed to the automaton definition, an algebraic parameter is used, as indicated by the alg keyword. An algebraic parameter is very similar to an algebraic variable, except that the parameter is not given a defining expression. Instead, the instantiation provides the expression. In the example above, fixed values are given, but these could also be computations, similar to how the defining expressions of algebraic variables can also be computations. When an automaton definition with an algebraic parameter is instantiated, a copy of the automaton definition is made, which is a concrete automaton. Within that copy, an algebraic variable is put with the same name and type as the algebraic parameter, and with the expression given in the instantiation as its defining expression. The parameter is then removed from the copy.

If there were a third bale loader helping out the farmer, and it has a capacity of 5 bales, the model could easily be extended by adding one line: bale_loader_tiny: BaleLoader(5).

Location parameters

Besides algebraic parameters, CIF also supports location parameters. These are similar to algebraic parameters, but only allow locations to be passed via instantiations. For instance, consider the following example:

                        
                            plant def Button():
                                uncontrollable u_pushed, u_released;

                                location Released:
                                    initial;
                                    marked;
                                    edge u_pushed goto Pushed;

                                location Pushed:
                                    edge u_released goto Released;
                            end

                            button1: Button();
                            button2: Button();

                            plant def Motor(location allow_on, allow_off):
                                controllable c_turn_on, c_turn_off;

                                location Off:
                                    initial;
                                    marked;
                                    edge c_turn_on  when allow_on  goto On;
                                location On:
                                    edge c_turn_off when allow_off goto Off;
                            end

                            motor1: Motor(button1.Pushed, button1.Released);
                            motor2: Motor(button2.Pushed, button2.Released);
                        
                    

The Button automaton definition models a simple button that can be pushed and released. It is instantiated twice, leading to two buttons: button1 and button2. The Motor automaton definition models a simple motor, that can be turned on and off. It is parameterized with two location parameters: allow_on indicates when it is allowed to turn on the motor, and allow_off indicates when it is allowed to turn off the motor. The location parameters are used to guard the edges for the c_turn_on and c_turn_off event, respectively. They only allow the motor to be turned on if the allow_on location is the current location of the automaton that contains it, and similarly for turning the motor off. There are two automaton instantiations for the motor: motor1 and motor2. For motor1, location Pushed of automaton instantiation button1 is pass as argument for parameter allow_on. This means that motor1 can only be turned on if button1 is pushed. And something similar is done for motor2 and button2, as well as for the motors to be allowed to be turned off.

In this example, the location allow_on parameter could easily be changed to alg bool allow_on. The model would then have the same behavior.

Event parameters

CIF also features event parameters that allow passing different events to automaton definitions, which can then be used on edges. Consider for instance the following example:

                        
                            automaton def ConveyorBelt(event accept, provide):
                                location NoProduct:
                                    initial;
                                    marked;
                                    edge accept goto HasProduct;

                                location HasProduct:
                                    edge provide goto NoProduct;
                            end

                            event start, move1to2, move2to3, move3to4, exit;

                            belt1: ConveyorBelt(start, move1to2);
                            belt2: ConveyorBelt(move1to2, move2to3);
                            belt3: ConveyorBelt(move2to3, move3to4);
                            belt4: ConveyorBelt(move3to4, exit);
                        
                    

The ConveyorBelt models a conveyer belt. Initially, it has no product, but it can accept a product and move it over its belt. Then once the product is at the end, it can provide the product to the next belt in production line. It is parameterized with two events: accept to accept a product onto the belt, and provide to provide its product to the next belt. Five events are defined in the model. Event start is used to start the system and move a product to the first belt. Event move1to2 moves a product from the first belt to the second belt. Events move2to3 and move3to4 are similar. Event exit is used to accept the product from the last belt, allowing it to exit the system. Four automaton instantiations of the ConveyorBelt automaton definition are defined. They pass the relevant events as arguments, such that the products are properly transferred from one belt to another. For instance, belt2 passes event move2to3 for the provide parameter, as it provides the product from belt2 to belt3. And belt3 passes that same event for the accept parameter, as it accepts the product from belt2. This way, both belt2 and belt3 have an edge for event move2to3. They synchronize on that event, and thus together perform a transition for that event. This way, a product is provided by belt2 and accepted by belt3 in a single transition, leading to a handover of the product from the second to the third belt.

Multiple parameters

In the conveyer belt example, two event parameters were defined using event accept, provide. Multiple algebraic or location parameters can be defined similarly, such as: alg int x, y and location loc1, loc2. If different kinds of parameters are desired on a single automaton definition, they are separated by semicolons, like so: alg int x, y; event e, f. Similarly, if different types of algebraic parameters are to be defined, they too are separated by semicolons: alg int a, b; alg bool c, d. The two event parameters of the conveyor belt example could also have been written as event accept; event provide, but event accept, provide is shorter and therefore preferred.

Groups

When modeling a large system, it can be useful to add more structure to it. CIF features groups, named collections of automata and other declarations.

For example, consider a road intersection at two crossing two-directional roads. Each of the four directions (north, east, south and west) has traffic lights for going left, straight ahead and right. So, there are twelve traffic lights. This system could be modeled in CIF as follows:

                        
                            automaton def LeftTrafficLight():
                                ...
                            end

                            automaton def StraightTrafficLight():
                                ...
                            end

                            automaton def RightTrafficLight():
                                ...
                            end

                            group north:
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end

                            group east:
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end

                            group south:
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end

                            group west:
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end
                        
                    

The use of automaton definitions and instantiations prevents having to copy the various traffic light automata many times. The bodies the automaton definitions are left out here, as they are not relevant for showing the concept of groups. The use of groups makes this CIF model structured and easy to read.

Groups may not only contain automaton instantiations, but also automata, events, constants, algebraic variables, or any combination of them that you think conceptually belong together. In fact, groups may contain whatever is allowed to be specified in models outside automata. In a way, the model as whole could be seen as an implicit group.

To refer to something that is declared inside a group, prefix the name of the declaration with the name of the group and a period. For instance, we could refer to the southern left traffic light by south.left. And if left traffic lights have an On location, then we could refer to the one for the south left traffic light by south.left.On.

Group definitions

The traffic light model above is already somewhat structured, but it can still be improved. The four groups are identical and only differ in name. To change something in the groups, it has to be changed separately in all groups, which is burdensome. And when changing one of them, it is easy to forget to update the other groups.

Similar to how automaton definitions can be used to reuse automata, group definitions can be used to reuse groups. Group definitions are thus templates for groups that can be instantiated multiple times. Group definitions can have the same kind of parameters as automaton definitions, and they are also instantiated in the same way. Similar to how automaton definitions are not automata, group definitions are not groups, but instantiated group definitions are. The following model shows how the traffic lights model can be simplified further using a group definition:

                        
                            automaton def LeftTrafficLight():
                                ...
                            end

                            automaton def StraightTrafficLight():
                                ...
                            end

                            automaton def RightTrafficLight():
                                ...
                            end

                            group def TrafficLights():
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end

                            north: TrafficLights();
                            east:  TrafficLights();
                            south: TrafficLights();
                            west:  TrafficLights();
                        
                    

All duplication is removed from the model. The model has more structure, is simpler and easier to read.

Components

In CIF, automata and groups are together called components. The entire model is the largest component. It can be subdivided into groups, which are sub-components. Groups can be nested, to create sub-sub-components, and so on. The model and any (sub-)groups in it, may contain automata. An automaton in the model is a sub-component, an automaton in a group in the model is a sub-sub-component, and so on. As automata and groups are together called components, and both allow definitions and instantiations, this concept is often referred to as the component definition/instantiation concept.

Component parameters

Besides algebraic, location and event parameters, CIF also features component parameters. This allows an entire component to be provided as a parameter to a component definition. For instance, consider again the button/motor example above. The motor is given the two locations of the button separately. If we use a component parameter, only one parameter is needed:

                        
                            plant def Button():
                                uncontrollable u_pushed, u_released;

                                location Released:
                                    initial;
                                    marked;
                                    edge u_pushed goto Pushed;

                                location Pushed:
                                    edge u_released goto Released;
                            end

                            button1: Button();
                            button2: Button();

                            plant def Motor(Button button):
                                controllable c_turn_on, c_turn_off;

                                location Off:
                                    initial;
                                    marked;
                                    edge c_turn_on  when button.Pushed   goto On;
                                location On:
                                    edge c_turn_off when button.Released goto Off;
                            end

                            motor1: Motor(button1);
                            motor2: Motor(button2);
                        
                    

Automaton definition Motor has a component parameter named button that expects an instance of the Button component definition to be passed to it. For motor1 the instantiated component button1 is provided, while for motor2 the argument is button2. Within the Motor definition, the elements of the Button definition can be accessed, such as its locations. You can see examples in the guards of the edges, such as button.Pushed, which refers to the Pushed location of the button.

Imports

So far, we have prevented duplication within a model, by using constants and algebraic variables for values that are used multiple times, and by using component definitions and instantiations for similar components. But, what about duplication between different models? CIF supports imports, that allow you to divide a model over multiple files. You can import one model in the other, to make sure they are together one model again.

Consider for instance two road intersections. One we saw earlier, and it has north, east, south and west directions. The other has only three directions: north, east and south. The definitions of the left, straight ahead and right traffic lights are the same. They can thus be shared between the models for the different intersections. That is, we could model the two intersections, using the following three CIF models:

File definitions.cif contains the common definitions:

                        
                            automaton def LeftTrafficLight():
                                ...
                            end

                            automaton def StraightTrafficLight():
                                ...
                            end

                            automaton def RightTrafficLight():
                                ...
                            end
                        
                    

File intersection4.cif models the intersection with 4 directions:

                        
                            import "definitions.cif";

                            group def TrafficLights():
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end

                            north: TrafficLights();
                            east:  TrafficLights();
                            south: TrafficLights();
                            west:  TrafficLights();
                        
                    

File intersection3.cif models the intersection with 3 directions:

                        
                            import "definitions.cif";

                            group north:
                                left:     LeftTrafficLight();
                                straight: StraightTrafficLight();
                            end

                            group east:
                                left:     LeftTrafficLight();
                                right:    RightTrafficLight();
                            end

                            group south:
                                straight: StraightTrafficLight();
                                right:    RightTrafficLight();
                            end
                        
                    

The definitions.cif file contains the common definitions. These are imported into the other models using an import declaration. An import can be thought of as being replaced by the content of the imported file.

The import keyword is followed by the file name or path to the file to import. The file name or path is enclosed in double quotes (") and followed by a semicolon (;). To import a CIF file from another directory, an import like import "directory/file.cif"; can be used. It is recommended to use / as separator, to make sure models work on all platforms (Windows, Linux, macOS).

Another common use of imports, is for structuring large models. Each sub-system can then be put in a different model. And the sub-systems are then all imported into the main system model.

Quiz