Version:
v9.0-RC1
[release notes]

# Module 3.5: Exercises

You will now practice what you have learned in this third 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 the following plant state space.

a. Is the following supervisor a proper supervisor for this plant, that ensures the controlled system is controllable, non-blocking and maximally permissive?

Hint: Compute the controlled system state space to answer this question.

##

The controlled system state space looks like this:

This controlled system is controllable:

- The plant allows events `push_start` and `push_stop` in every state, and so does the supervisor. Since they are enabled in every state of the plant and the supervisor, they are also enabled in every state of the controlled system.
- Event `turn_on` is only enabled in state `C` of the plant. In the single controlled system that matches plant state `C`, the event is also enabled.
- And the controlled system similarly does not restrict the occurrence of event `turn_off` compared to the plant.

In fact, the supervisor only restricts event `start_machine` from occurring in controlled system state `(B, 3)`.

The supervisor automaton itself is non-blocking. However, the controlled system has many blocking states.

The controlled system is not maximally-permissive. To understand why this is the case, consider the following:

- The plant is already non-blocking, so no states need to be removed to ensure the controlled system is non-blocking.
- With no blocking states to remove, also no states need to be removed to ensure controllability.
- In fact, no additional restrictions are needed, and thus the plant itself is its own maximally-permissive supervisor.

With the plant itself being a proper maximally-permissive supervisor, it is easy to see that the given supervisor, and its controlled behavior, are not maximally permissive: the plant can go through many start-stop cycles, while the controlled system can only go through one.

b. What would happen if in location `3` of the supervisor the edge for event `push_stop` were to be removed? Would it then be a proper supervisor?

Hint: Compute the new controlled system state space.

##

The new controlled system state space is depicted below. The red arrows and labels indicate what is removed compared to the previous controlled system state space:

The controlled system is then no longer controllable, since the `push_stop` event is then disabled in various states of the controlled system, compared to the uncontrolled system (in states with red events on outgoing transitions). It still has blocking states and thus is still blocking. It also still restricts the `start_machine` event and is thus not maximally permissive.

c. Is the following alternative supervisor a proper supervisor for the plant?

##

Yes, this is a proper supervisor. The supervisor does not restrict the plant: the state space of the plant is the same as the state space of the controlled system (the plant combined with the supervisor).

d. Apply the synthesis algorithm, using the controlled system state space from the solution to Exercise 1a as plant.

##

The blocking behavior starts at state `(C, 3)`, so states `(C, 3)`, `(F, 2)`, `(E, 1)`, `(D, 3)`, `(A, 3)` and `(B, 3)` are removed. To make sure state `(C, 3)` is not reached, event `start_machine` is disabled in state `(B, 2)`. Nothing needs to be removed to ensure controllability. The resulting non-blocking, controllable, maximally-permissive supervisor is:

Note that this supervisor has alphabet `push_start`, `push_stop`, `turn_on`, `turn_off`, `start_machine`, `stop_machine`. Out of the six events, only two are allowed by the supervisor, and thus in the controlled system. It never allows uncontrollable events `turn_on` and `turn_off`, but this is theoretically OK, since the plant states where these events are enabled can't be reached. Whether this supervisor makes sense for the actual system we don't know, as we did not explain the system and its purpose. Generally though, it is a sign of a problem if one ore more events of the system are not enabled in any of the states of the controlled system.

## Exercise 2

Synthesize a proper supervisor for the following plant:

##

For the first iteration of the synthesis algorithm:

1. Blocking state `6` is removed.
2. Since removed state `6` has an incoming transition for uncontrollable event `d`, state `8` is removed.
3. Unreachable state `7` is removed.
4. The `a` and `c` transitions from state `5` and the `c` transition from state `3` are removed.

For the second iteration of the synthesis algorithm:

1. There are no blocking states.
2. Since removed state `8` has an incoming transition for uncontrollable event `d`, state `4` is removed.
3. There are no unreachable states.
4. The `c` transition from state `1` and the `b` transition from state `5` are removed.

For the third iteration of the synthesis algorithm:

1. Blocking state `5` is removed.
2. There are no non-controllable states.
3. There are no unreachable states.
4. The `c` transition from state `2` and the `e` transition from state `3` are removed.

The fourth iteration of the synthesis algorithm does not lead to any changes.

The resulting supervisor is:

## Exercise 3

Consider again the clothing company from a question of the quiz of the previous sub-module, and the answer to that question. Also consider that all of the company's machines are like the machine with a button and a motor, from the example of the controllability synthesis guarantee.

a. Model the clothing company as a plant model in CIF.

##

The model structure of component definitions/instantiations and group is taken from the quiz question's answer. The `Machine` group definition contains the plant automata. The controllable and uncontrollable have been given names that start with `c_` and `u_`, respectively. They are then highlighted in different colors.

                                                group def Machine():
                                                    plant button:
                                                        uncontrollable u_push, u_release;

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

                                                        location Pushed:
                                                            edge u_release goto Released;
                                                    end

                                                    plant motor:
                                                        controllable c_turn_on, c_turn_off;

                                                        location Off:
                                                            initial;
                                                            marked;
                                                            edge c_turn_on goto On;

                                                        location On:
                                                            edge c_turn_off goto Off;
                                                    end

                                                    plant interactions:
                                                        location Released:
                                                            initial;
                                                            marked;
                                                            edge button.u_push goto Pushed;
                                                            edge motor.c_turn_off;

                                                        location Pushed:
                                                            edge button.u_release goto Released;
                                                            edge motor.c_turn_on;
                                                    end
                                                end

                                                group def Hall():
                                                    machine1: Machine();
                                                    machine2: Machine();
                                                    machine3: Machine();
                                                    machine4: Machine();
                                                end

                                                group def Factory():
                                                    hall1: Hall();
                                                    hall2: Hall();
                                                end

                                                group def Country():
                                                    factory1: Factory();
                                                    factory2: Factory();
                                                end

                                                country1: Country();
                                                country2: Country();
                                                country3: Country();

b. Due to regulations, the machines have to be checked regularly. Adapt the CIF model based on the following regulations and constraints.

Regulations:

- Machines have to be checked after they have been used a certain number of times (we call this the `limit`). The regulations differ in each country. In countries 1 it has to be checked after it has been used 6 times. In country 2, it is after 8 times. And in country 3, after 9 times.
- An operator of a machine may decide to stall a check until the factory is less busy.

Modeling constraints:

- Parameterize the definitions such that the you only have to enter the `limit` at the country instantiations.
- Model the checking of a machine by means of a single extra plant automaton, without adapting the existing plant automata.
- Declare the event `check_start` to indicate a machine is being checked and `check_passed` to indicate it passed the check.
- Make sure the new events are either controllable or uncontrollable.
- While a machine is being checked, it must be off.

##

An algebraic parameter `limit` is defined on all group definitions, to allow passing it from each country to each factory, hall and machine. A single automaton named `check` is added to the `Machine`. It can directly access the `limit` parameter of the `Machine`.

The `c_check_start` and `c_check_passed` events are modeled as uncontrollable events. The operator decides when to start checking, and may delay it. The operator also decides when a machine has passed a check. A supervisory controller can't prevent the operator from doing so, and thus the events are uncontrollable from the perspective of the supervisor.

The number of times the machine has been used is counted in `used`. This number is increased each time the machine is turned off.

To keep track of whether the country-specific `limit` has been reached, an algebraic variable `limit_reached` is declared. Since the operator may delay checking the machine, `limit_reached` is defined as `used >= limit` rather than as `used = limit`. This allows using the value of the algebraic variable to decide whether an operator may start to check the machine.

The automaton has two locations. Initially, the system is `NotChecking`. Once the operator starts the check, the automaton goes to the `Checking` location. The operator may only start the check using the `u_check_start` event when the `limit_reached` condition holds. To make sure the motor is off when the operator starts to check the machine, the `u_check_start` event is additionally guarded by the `motor.Off` condition. To make sure the motor stays off while the operator is checking the machine, the `motor.c_turn_on` event is only allowed in the `Running` location, and not in the `Checking` location. Since the motor is off in the `Checking` location, there is no need to allow the `motor.c_turn_off` event there. Once the motor has passed the check, the automaton goes back to the `NotChecking` location. The `used` count is then reset.

                                                group def Machine(alg int limit):
                                                    plant button:
                                                        uncontrollable u_push, u_release;

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

                                                        location Pushed:
                                                            edge u_release goto Released;
                                                    end

                                                    plant motor:
                                                        controllable c_turn_on, c_turn_off;

                                                        location Off:
                                                            initial;
                                                            marked;
                                                            edge c_turn_on goto On;

                                                        location On:
                                                            edge c_turn_off goto Off;
                                                    end

                                                    plant interactions:
                                                        location Released:
                                                            initial;
                                                            marked;
                                                            edge button.u_push goto Pushed;
                                                            edge motor.c_turn_off;

                                                        location Pushed:
                                                            edge button.u_release goto Released;
                                                            edge motor.c_turn_on;
                                                    end

                                                    plant checking:
                                                        uncontrollable u_check_start, u_check_passed;
                                                        disc int used = 0;
                                                        alg bool limit_reached = used >= limit;

                                                        location NotChecking:
                                                            initial;
                                                            marked;
                                                            edge motor.c_turn_off do used := used + 1;
                                                            edge motor.c_turn_on;
                                                            edge u_check_start when limit_reached and motor.Off goto Checking;

                                                        location Checking:
                                                            edge u_check_passed do used := 0 goto NotChecking;
                                                    end
                                                end

                                                group def Hall(alg int limit):
                                                    machine1: Machine(limit);
                                                    machine2: Machine(limit);
                                                    machine3: Machine(limit);
                                                    machine4: Machine(limit);
                                                end

                                                group def Factory(alg int limit):
                                                    hall1: Hall(limit);
                                                    hall2: Hall(limit);
                                                end

                                                group def Country(alg int limit):
                                                    factory1: Factory(limit);
                                                    factory2: Factory(limit);
                                                end

                                                country1: Country(6);
                                                country2: Country(8);
                                                country3: Country(9);

c. Adapt the motor automaton in your CIF model such that the interactions automaton can be removed.

##

The relations automaton ensures the motor can only be turned on while the button is pushed, and can only be turned off while the button is released. This can also be modeled using guards.

                                                plant motor:
                                                    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

## Exercise 4

Consider a system with three machines. For a machine to be started, one of the other machines must be on. Machine 2 can only be started when machine 1 is on, machine 3 can only be started when machine 2 is on, and machine 1 can only be started when machine 3 is on. There is thus a sort of cyclic dependency between the machines.

The machines can be modeled using the following three automata (machine 1 at the top left, machine 2 at the top right, machine 3 at the bottom). Machine 1 can be started with the `s1` event, and it can be turned off using the `o1` event. When machine 1 is `On`, it enables starting machine 2, by means of the self loop for the `s2` event. The other two machines are modeled similarly.

a. Model this system in CIF, compute its state space, and depict it graphically, using CIF tools.

##

The system can be modeled in CIF as follows:

                                                controllable o1, s1;
                                                controllable o2, s2;
                                                controllable o3, s3;

                                                plant machine1:
                                                    location On:
                                                        initial;
                                                        marked;
                                                        edge s2;
                                                        edge o1 goto Off;

                                                    location Off:
                                                        edge s1 goto On;
                                                end

                                                plant machine2:
                                                    location On:
                                                        initial;
                                                        marked;
                                                        edge s3;
                                                        edge o2 goto Off;

                                                    location Off:
                                                        edge s2 goto On;
                                                end

                                                plant machine3:
                                                    location On:
                                                        initial;
                                                        marked;
                                                        edge s1;
                                                        edge o3 goto Off;

                                                    location Off:
                                                        edge s3 goto On;
                                                end

Note that no `c_` prefixes are used, to keep the names of the event as described. This means the event names are not colored, but remain black.

The state space can use computed using the CIF explorer, and be visualized using the CIF to yEd transformer:

b. Is a supervisor needed? Explain your answer.

##

If all three machines are off at the same time, the system is in a deadlock. A supervisor should be synthesized to prevent this deadlock.

c. Manually synthesize a supervisor for this system, by following the steps of the synthesis algorithm. What restrictions does the synthesized supervisor impose?

##

The synthesized supervisor looks like this:

The state where all three machines are off, is removed. All the transitions leading to this state are disabled. For instance, when only machine 3 is on, the event to turn machine 3 off is disabled.

d. Remodel the system, making use of the fact that the three plant automata are very similar, while preserving the state space.

Hint: The three machine automata are the same except for the events they use on the edges. Use one plant automaton definition with event parameters and three instantiations.

##

The three instantiations have the same names as the original automata, to ensure the components' names are preserved.

                                                controllable o1, s1;
                                                controllable o2, s2;
                                                controllable o3, s3;

                                                plant def Machine(controllable start, off, allow):
                                                    location On:
                                                        initial;
                                                        marked;
                                                        edge allow;
                                                        edge off goto Off;

                                                    location Off:
                                                        edge start goto On;
                                                end

                                                machine1: Machine(s1, o1, s2);
                                                machine2: Machine(s2, o2, s3);
                                                machine3: Machine(s3, o3, s1);

## Exercise 5

You are going to model cannibalistic rabbits. The rabbits have locked themselves in their rabbit hole and can't get any food. So, the rabbits start feeding on each other. Luckily, two rabbits can reproduce, leading to a new rabbit in the rabbit hole, ensuring food security in the long run. The rabbit hole can only house 4 rabbits. The initial population size is 3 rabbits. Furthermore, the rabbits can eat themselves out of desperation when no other rabbits are left.

Model the population size of the rabbits as a plant model, on paper. Also, derive a supervisor if necessary.

##

The population size can be modeled as a plant as follows:

Once there are less than two rabbits, the population will die out, resulting in deadlock. A supervisor should therefore be synthesized that prevents the rabbit from eating each other when the population size is two. Though, good luck explaining this to a rabbit. We opt to make all stable states marked. The synthesized supervisor is then as follows:

## Exercise 6

Model the plant state space from the example on which the synthesis algorithm was explained earlier in this module, as a single CIF automaton. In the same CIF model, model the final three-state supervisor that was synthesized for it.

Then, check whether it makes a difference if the alphabet of the supervisor is the same as the plant or is `b`, `d`, `e`, f.

Hints:

- Define all events globally and define explicit alphabets for both automata.
- Ignore any warnings about certain events not being used on any edge.
- Compute the state spaces of both controlled systems and compare them, to see whether the different alphabets matter.

##

The plant state space, together with the supervisor with the full plant alphabet, can be modeled as follows in CIF:

                                                controllable a, b, c, d, e;
                                                uncontrollable f;

                                                plant p:
                                                    alphabet a,b,c,d,e,f;

                                                    location l11:
                                                        edge c goto l21;
                                                        edge e goto l31;

                                                    location l21:
                                                        edge d goto l11;
                                                        edge b goto l22;
                                                        edge f goto l31;

                                                    location l22:
                                                        initial;
                                                        edge a goto l21;
                                                        edge b;
                                                        edge d goto l12;
                                                        edge f goto l32;

                                                    location l12:
                                                        edge a goto l11;
                                                        edge e goto l32;

                                                    location l31:
                                                        edge e;

                                                    location l32:
                                                        marked;
                                                        edge a goto l31;
                                                        edge e;
                                                end

                                                supervisor s:
                                                    alphabet a, b, c, d, e, f;

                                                    location l22:
                                                        initial;
                                                        edge b;
                                                        edge d goto l12;
                                                        edge f goto l32;

                                                    location l12:
                                                        edge e goto l32;

                                                    location l32:
                                                        marked;
                                                        edge e;
                                                end

The variant where the supervisor has a smaller alphabet can be obtained by changing the explicit alphabet declaration of supervisor automaton `s`.

When the alphabet of the plant and supervisor are the same, the supervisor is a proper supervisor. It then disables all relevant events, resulting in the correct controlled system state space. When the supervisor alphabet is reduced, certain events are no longer restricted by the supervisor, and the controlled system contains undesired behavior.