Version:
v7.0
[release notes]

# Module 2.8: Exercises

You will now practice what you have learned in this second module. When modeling, there is generally not one correct answer, as multiple solutions are possible. After you complete an exercise, an example solution is given, together with an explanation.

## Exercise 1

Consider again the example model with a bridge deck, bridge light and car, from the constants and algebraic variables sub-module. Compute the state space of the model using the CIF explorer. Visualize the state space by converted the state space CIF model to a yEd model diagram, opening it in yEd, and applying One-Click Layout. Why does the state space have 20 states and 56 transitions?

##

The angle of the bridge deck can vary between 0 and 90 degrees, for a total of 10 different angles. The bridge light can be either on or off. These can be combined in any combination, so there are 10 * 2 = 20 states.

From most states, it is possible to both open the bridge deck further and close it further. From all states, it is possible to either turn the bridge on or off. For most states, there are thus three possible transitions. There are a few states that are exceptional in this regard. For the states where the bridge deck is fully open, is is not possible for the bridge deck to be opened any further. Similarly, for the states where the bridge deck is fully closed, is is not possible for the bridge deck to be closed any further. In total there are four states with only two transitions, namely those where the bridge deck is fully opened or closed, in combination with the bridge light being either on or off. This means that there are thus (20 * 3) - 4 = 56 transitions.

You may have noticed that the state space model has groups. Groups can be used to group automata, event declarations and so on, bringing structure to a model. In this case, the groups are used to preserve the structure of the original model. The original automata are replaced by groups, such that the events declared inside of them are still grouped as in the original model. To refer to an event declared in a group, from outside that group, the event name needs to be prefixed with the name of the group and a period, like when referring to an event declared in an automaton from outside that automaton. Groups are further explained later in the course.

## Exercise 2

Consider again the example model with a bridge deck, bridge light and car. Check again the state space or simulate the model.

a. Does the model have any unsafe behavior?

Hint: Consider whether all transitions are desired.

##

Yes, the model has unsafe behavior. The bridge deck and bridge light operate independently. They don't synchronize on any events, nor do they share any variables. The bridge deck can therefore be opened, while the bridge light is off.

The `car_may_drive` and `car_may_not_drive` variables correctly indicate whether the car may or may not drive. But, what happens when the driver is not paying attention to whether to bridge deck is open or closed, and only looks at the bridge light? In that case, the car would drive into the water. It would be safer if the bridge light were always on when the bridge deck is not fully closed. So, all states where the bridge deck is not fully closed and the bridge light is off should not be reachable.

b. Change the model to make it safe, by adding guards to the relevant edges.

##

The bridge light must be on for the bridge deck to be opened. Furthermore, the bridge light should only be turned off when the bridge is fully closed. Below is an example of how of how the model can be made safe.

The `open_further` and `close_further` edges are guarded with the bridge light being on, to ensure the bridge deck does not move when the bridge light is off. Instead of using the location in the guard, we could have also opted for the algebraic boolean variable `is_on`. The `turn_off` event is guarded with the bridge deck being closed. Here too, we used the algebraic variable, rather than directly using `angle`, since this gives better abstraction and leads to a more readable model.

                                                automaton bridge_deck:
                                                    disc int angle = 0;
                                                    event open_further, close_further;

                                                    const int step = 10;

                                                    alg bool is_open   = angle >= 90;
                                                    alg bool is_closed = angle <= 0;

                                                    location:
                                                        initial;
                                                        edge open_further  when angle < 90 and bridge_light.On do angle := angle + step;
                                                        edge close_further when angle >  0 and bridge_light.On do angle := angle - step;
                                                end

                                                automaton bridge_light:
                                                    event turn_on, turn_off;

                                                    alg bool is_on = On;
                                                    alg bool is_off = Off;

                                                    location On:
                                                        initial;
                                                        edge turn_off when bridge_deck.is_closed goto Off;

                                                    location Off:
                                                        edge turn_on goto On;
                                                end

                                                alg bool car_may_drive     =     bridge_deck.is_closed and bridge_light.is_off;
                                                alg bool car_may_not_drive = not bridge_deck.is_closed or  bridge_light.is_on;

## Exercise 3

Compute the state space of some examples manually, without using any tools, such as the CIF explorer.

a. Compute the state space of the driver and mechanic example from the synchronizing automata sub-module.

##

b. Compute the state space of the two-automata example from the quiz of the synchronizing automata sub-module.

##

c. Compute the state space of the production line from the shared variables sub-module, with at most one product in the system, and any non-empty batch is allowed to be sent.

##

## Exercise 4

Consider the models for which you computed the state spaces in exercises 3a and 3b. Answer for both of them the following questions:

- Are there any deadlock states?
- Are all the locations of the automata reachable?
- Is the state space non-blocking?

##

For the solution to exercise 3a:

- No, there are no deadlock states, as every reachable state has an outgoing transition.
- Yes, since all three locations of `Driver` and all three locations of `Mechanic` are reachable.
- Yes, since the initial state is marked, and it is always possible to get back to the initial state.

For the solution to exercise 3b:

- No, there are no deadlock states, as every reachable state has an outgoing transition, including `loc3`, which has a self loop transition.
- Yes, since all three locations of the top automaton and both locations of the bottom automaton are reachable.
- No. The `loc3` is not marked, and since it only has a self loop transition, no marked state can be reached from it. Furthermore, `loc6` is also not marked, and from it only the state itself (via a self loop) and `loc3` (via a transition for event `a`), can be reached. Neither of these two states is marked. Since there are two states, `loc3` and `loc6` that are not marked and from which no marked state can be reached, the model is blocking.

## Exercise 5

Consider again the product line from the shared variables sub-module. Make a CIF model for it. Check that it has the correct behavior, using simulation and by computing and visualizing the state space.

##

                                                automaton buffer:
                                                    event take_product, send_batch;
                                                    disc int products = 0;

                                                    location Receiving:
                                                        initial;
                                                        marked;
                                                        edge take_product when products < 10 do products := products + 1;
                                                        edge send_batch when products > 4 goto Sending;

                                                    location Sending:
                                                        edge even_packer.batch_to_even, odd_packer.batch_to_odd goto Receiving;
                                                end

                                                automaton decision_unit:
                                                    location Idle:
                                                        initial;
                                                        marked;
                                                        edge buffer.send_batch goto Deciding;

                                                    location Deciding:
                                                        edge even_packer.batch_to_even when buffer.products mod 2 = 0 goto Idle;
                                                        edge odd_packer.batch_to_odd when buffer.products mod 2 = 1 goto Idle;
                                                end

                                                automaton even_packer:
                                                    event batch_to_even, finish_even;

                                                    location Idle:
                                                        initial;
                                                        marked;
                                                        edge batch_to_even goto Packing;

                                                    location Packing:
                                                        edge finish_even goto Idle;
                                                end

                                                automaton odd_packer:
                                                    event batch_to_odd, finish_odd;

                                                    location Idle:
                                                        initial;
                                                        marked;
                                                        edge batch_to_odd goto Packing;

                                                    location Packing:
                                                        edge finish_odd goto Idle;
                                                end

## Exercise 6

Consider again exercise 4 from the exercises of Module 1. When you look at the solution of that exercise, you can now recognize that it is actually the state space of a model with two automata. You can see this most prominently by the fact that the locations are named as pairs consisting of the names of the current locations of the two automata.

Identify the two automata for which the solution is the state space. Model the two automata as a CIF model, without using variables. Check that the behavior of your CIF model is the same as the state space that is given as the solution in exercise 4 of Module 1. Also check the behavior against the model that you made in exercise 8 of Module 1, where you modeled the single automaton in CIF, and make sure it is the same.

##

                                                automaton lamp:
                                                    event turn_on, turn_off;

                                                    location Off:
                                                        initial;
                                                        marked;
                                                        edge turn_on when counter.Zero or counter.Two or counter.Four goto On;

                                                    location On:
                                                        edge turn_off goto Off;
                                                end

                                                automaton counter:
                                                    event increment, decrement;

                                                    location Zero:
                                                        initial;
                                                        marked;
                                                        edge increment when lamp.Off goto One;

                                                    location One:
                                                        edge decrement goto Zero;
                                                        edge increment goto Two;

                                                    location Two:
                                                        edge decrement when lamp.Off goto One;
                                                        edge increment when lamp.Off goto Three;

                                                    location Three:
                                                        edge decrement goto Two;
                                                        edge increment goto Four;

                                                    location Four:
                                                        edge decrement when lamp.Off goto Three;
                                                end

## Exercise 7

You will model the interaction between two hay balers and a bale loader.

A hay baler is a farming machine that makes square or round bales, depending on the type, of hay or straw. A baler makes a bale on event `make_bale` and has a counter that counts how many bales have been made so far (variable name `bales`). The two balers are identical and work independently of each other.

The bale loader is a machine that loads the bales and brings them to the farm. It has a capacity of 10 bales and only collects them when enough bales are present. Collecting the 10 bales, by event `load_bales`, can be modeled as happening instantaneously when enough bales are present on the field. The bale loader also has a counter that keeps track of how many bales have been loaded so far (variable name `loaded_bales`).

a. Model this system in CIF using multiple automata.

Keep the following in mind:

- The load capacity of the loader should be easily adjustable.
- Define an integer variable named `bales_on_field` that automatically keeps track of the number of bales still on the field.
- Define a boolean variable that automatically indicates to the loader whether enough bales are on the field to start loading.

##

The balers each have their own `make_bale` event, to make sure they operate independently. These events belong logically to the balers, and are thus defined locally. The balers can make bales, increasing the amount of bales they've made by one.

The bale loader has a constant to define its capacity, allowing it to be easily changed. This constant is placed in the `bale_loader` automaton, as it indicates a property of the bale loader. Similarly to how the balers count the number of bales they've made, the loader counts the number of bales its loaded.

Algebraic variable `bales_on_field` counts the number of bales on the field, as the different between the baled bales and the loaded bales. This variable is defined globally, since it relates to both balers and bale loader and the field that they share, rather than any one of them in particular.

The loader uses the `bales_on_field` variable to define `enough_bales` that indicates whether enough bales are on the field to load the loader to capacity. This variable is also defined locally for the bale loader, as it indicates a condition for the bale loader, and it is used only by the bale loader. The edge for the `load_bales` event is guarded with this variable to ensure that the loader operates correctly.

                                                alg int bales_on_field = baler1.bales + baler2.bales - bale_loader.loaded_bales;

                                                automaton baler1:
                                                    event make_bale;
                                                    disc int bales = 0;

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

                                                automaton baler2:
                                                    event make_bale;
                                                    disc int bales = 0;

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

                                                automaton bale_loader:
                                                    event load_bales;
                                                    disc int loaded_bales = 0;

                                                    const int load_capacity = 10;
                                                    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;
                                                end

b. Adapt the model to make sure the loader can keep up with the balers.

Let's assume that the loader cannot keep up with the balers. Therefore, it tells them to stop when they have baled enough bales to meet its load capacity. The balers can only restart baling when the loader has loaded its bales.

Add an event `stop_baling` that informs both balers to stop baling. Do not introduce any other new events.

##

We introduce event `stop_bailing` outside the automata, as it is shared by multiple balers and the bale loader. Alternatively, we could have placed it in the bale loader, since it initiates the event, telling the bale loaders to stop baling.

The bale loader requires the event to take place only when enough bales have been baled.

The balers synchronize on the event and go to a different location, where they do not bale any more bales. Once the loader has loaded the bales, through event `load_bales`, the balers go back to their bailing location to continue bailing. To make sure that the balers do not make more bales when enough bales have been made for the loader to start loading, extra guards are added to the edges for the `make_bale` event.

                                                alg int bales_on_field = baler1.bales + baler2.bales - bale_loader.loaded_bales;

                                                event stop_baling;

                                                automaton baler1:
                                                    event make_bale;
                                                    disc int bales = 0;

                                                    location Baling:
                                                        initial;
                                                        marked;
                                                        edge make_bale when not bale_loader.enough_bales do bales := bales + 1;
                                                        edge stop_baling goto NotBaling;

                                                    location NotBaling:
                                                        edge bale_loader.load_bales goto Baling;
                                                end

                                                automaton baler2:
                                                    event make_bale;
                                                    disc int bales = 0;

                                                    location Baling:
                                                        initial;
                                                        marked;
                                                        edge make_bale when not bale_loader.enough_bales do bales := bales + 1;
                                                        edge stop_baling goto NotBaling;

                                                    location NotBaling:
                                                        edge bale_loader.load_bales goto Baling;
                                                end

                                                automaton bale_loader:
                                                    event load_bales;
                                                    disc int loaded_bales = 0;

                                                    const int load_capacity = 10;
                                                    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