Version:
v7.0
[release notes]

# 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

[ { type: 'single-choice', question: ` What is the difference, syntax-wise, between automata and automaton definitions? Is this the same as for groups and group definitions? `, answers: [ `Automaton definitions use the `def` keyword and between parentheses they can optionally have parameters. Automata do not have either of those. The same is true for groups and group definitions.`, `Automata use the `def` keyword and between parentheses they can optionally have parameters. Automaton definitions do not have either of those. The same is true for groups and group definitions.`, `Automaton definitions use the `def` keyword and between parentheses they can optionally have parameters. Automata do not have either of those. For groups and group definitions it is the other way around.`, ], correctAnswer: '1' }, { type: 'multiple-choice', question: "Which two kind of parameters can a definition take?", answers: [ "Algebraic parameters.", "Component parameters.", "Constant parameters.", "Discrete parameters.", "Event parameters.", "Guard parameters.", "Location parameters.", ], correctAnswer: '1, 2, 5, 7' }, { type: 'single-choice', question: "Why and when are groups useful?", answers: [ `When the system being modeled contains parts that the modeler thinks conceptually belong together. It improves the structure of the model and makes it easier to read and understand.`, "When the system being modeled is very big, groups are needed to keep the model functional and efficient.", `When the system being modeled belongs to a group of systems previously modeled, you add this model to the group. This structures the group of models.`, ], correctAnswer: '1' }, { type: 'single-choice', question: ` A clothing company does business in three different countries. It has two factories in each country. Each factory consists of two halls, and each hall houses four machines. How can this best be modeled in CIF?`, answers: [ `Automaton definitions for a hall and a machine. A group definition for a factory containing two hall automaton instantiations and two machine automaton instantiations. A group definition for a country containing two factory group instantiations. Three country group instantiations in the model.`, `An automaton definition for a machine. A group definition for a hall containing four machine automaton instantiations. A group definition for a factory containing two hall group instantiations. A group definition of a country containing two factory group instantiations. Three country group instantiations in the model.`, `An automaton definition for a machine. A group definition for a hall containing two machine automaton instantiations. A group definition for a factory containing three hall group instantiations. A group definition for a country containing four factory group instantiations. Two country group instantiations in the model.`, ], correctAnswer: '2' }, { type: 'multiple-choice', question: "What is a good use of the import concept, and how do you import a file?", answers: [ `When you want to import a file from somebody else, you use the import functionality to import it into your workspace. You import a file by typing the `import` keyword and the path to the file you want to import between double quotes.`, `When a model becomes very large and covers multiple parts of a system, you can divide it into separate files to structure it. You import a file by typing the `import` keyword and the path to the file you want to import between double quotes.`, `When your model becomes too large, you have to divide the model into multiple files to ensure the tools keep running efficiently. You import a file by typing the `import` keyword and the path to the file you want to import between double quotes.`, `When you want to reuse a part of your model in another model, you can separate out the common part to another file, and import it into both models. You import a file by typing the `import` keyword and the path to the file you want to import between double quotes.` ], correctAnswer: '2, 4' } ]