Version:
v9.0-RC1
[release notes]

# Module 1.5: Exercises

You will now practice what you have learned in this first 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

A vending machine will give you the snack that you want, after you give it a coin (event `give_coin`). If you put in an additional coin, while it is processing your order, it will reject this coin and give it back (event `reject_coin`). Once the vending machine has delivered your order (event `deliver`), it will accept a next coin.

Model this vending machine using an automaton, by drawing it on paper. First, think of appropriate events and locations. Then, consider which locations should be initial and marked.

##

The machine is initially waiting for a customer to enter a coin, in location `Waiting`. Once it is given a coin, it is busy getting your order and will not accept another coin, in location `Busy`. If another coin is given, the automaton goes to a third location, `Rejecting`. In real life, the machine will only be in this location for a fraction of time, as it will immediately reject the second coin once it is given.

## Exercise 2

A coffee machine is initially waiting for an order. It requires input on what type of coffee it needs to make. Upon receiving an order, the coffee machine starts grinding the coffee. The machine heats the water subsequently and adds the water to the grinded coffee beans to extract the coffee from the beans. After delivering the coffee to the cup, the machine returns to waiting for an order. An emergency stop button can be pressed to stop the coffee machine directly, independent of its current state. Each time the coffee machine goes into emergency mode, it needs to be reset before it can start waiting for an order again.

Model this coffee machine using an automaton, by drawing it on paper.

##

The coffee machine is initially waiting for customers to enter their choice. Once a choice is made, it grinds the beans, heats the water and puts the two together to extract the coffee from the beans. Appropriate events are `make_choice`, `start_heating`, `add_water_to_beans`, `deliver`, `emergency` and `reset`. Appropriate states are `Wait`, `Grind`, `Heat` and `Extract`. You can, of course, name them differently. The emergency mode is modeled using location `Emergency`. The event `emergency` leads to this location, from every location. It is also possible to push the emergency stop button while the coffee machine is in emergency mode, so a self loop edge is needed for the `emergency` event in the `Emergency` location. Appropriate marked locations are `Wait` and `Emergency` (either or both).

## Exercise 3

Two persons, A and B, can use a bicycle. Only one person can use the bicycle at a time. Person A can start riding the bicycle by event `ride_A`, and similarly person B can start riding it by event `ride_B` When the person riding the bicycle is done riding it, the corresponding event `leave_A` (for person A) or `leave_B` (for person B) occurs.

Model this bicycle using an automaton, by drawing it on paper.

##

It is essential that the two persons don't use the bicycle simultaneously. So, a person needs to leave the bicycle, before the other person can start riding it. A person may also leave the bicycle and then start riding it again.

## Exercise 4

Model a counter that counts from zero to 4. The `increment` event increments the counter, and the `decrement` event decrements it. The counter is connected to a lamp, and it should be possible to turn the lamp on only when the counter has an even value. The counter can only change value when the lamp is off. Initially, the counter is zero.

Model this counter and lamp using an automaton without variables, by drawing it on paper.

##

## Exercise 5

Model again the counter and lamp from the previous exercise, by drawing it on paper, but now using variables, guards, updates, and exactly two locations. Hint: `i mod j` returns the remainder of `i` divided by `j`.

##

A variable named `count` can be used for the counter, instead of five different locations. A guard `count mod 2 = 0` for the `turn_on` event then makes sure that the lamp can only be turned on when the counter value divided by two has no remainder, and thus the counter has an even value. Two locations are used to represent that the lamp is on or off. In principle, if the exercise did not force us to use two locations, we could have opted for a single location. We could then have encoded the state of the lamp with a second variable.

## Exercise 6

A salesman at a market wants 0.45 euro for his product. He starts with 5 products in stock. You can pay in coins of 5 cent, 10 cent and 20 cent (denoted by events `pfive`, `pten` and `ptwenty`). When you give the salesman coins, he will check whether it is enough. If it is not enough, he will ask for more money (event `ask_more`). If it is enough, he will get the product for you (event `get_product`). While getting the product, he calculates the change (variable `cha`). Once he is done and knows how much money he needs to give back, he will give the surplus amount back with the product (event `deliver`).

Model this interaction with the salesman, in two different situations, by drawing them on paper. For both situations, include the cash amount you have (variable `yc`) and that the salesman has (variable `sc`). The amount of cash in both your pocket and the salesman's pocket should be known throughout the entire interaction. You start with 2.25 euro and cannot borrow money at any time, even when your pocket is empty. The salesman starts with no money. Also include the products in stock of the salesman (variable `ps`). You may leave out marking.

Situation 1: You give each coin directly to the salesman, and the salesman says when you gave enough. Hint: Introduce an extra variable.

##

Three locations are used: `Paying`, `Checking` and `Getting`. Euro amounts are represented in cents. Besides variables `yc`, `sc`, `ps` and `cha`, an extra variable named `given` is introduced. It represents the cash amount given to the salesman for the current purchase. When delivering, variable `given` is reset to zero, to start fresh for the next purchase. You could also model it differently, for instance keeping track of the money the salesman had prior to the current purchase. But remember that the cash amounts in both your pocket and the salesman's pocket should be known throughout the entire interaction.

Situation 2: You first collect your coins in your hand before you give them all to the salesman at once. Hint: Introduce an extra event.

##

Variable `hand` represents the amount of money in your hand. The edges for collecting money in your hand can be self loops. An extra event `give_money` is introduced for giving the money to the salesman. An edge with this event is added as well.

## Exercise 7

In the previous exercises, you modeled automata on paper. Now, you will model in CIF instead, and use simulation for validation.

7a: Model your solution to both situations of exercise 6 in CIF. Then simulate the CIF models to validate them, determining whether they are correct.

7b: Also make CIF models of the example solutions for both situations of exercise 6. If your own models are the same as those example solutions, you obviously do not have to model them again.

##

CIF model for example solution to exercise 6a:

                                                automaton market:
                                                    event pfive, pten, ptwenty, ask_more, get_product, deliver;
                                                    disc int yc = 225, sc = 0, ps = 5, given = 0, cha = 0;

                                                    location Paying:
                                                        initial;
                                                        edge pfive   do yc := yc - 5,  sc := sc + 5,  given := given + 5  goto Checking;
                                                        edge pten    do yc := yc - 10, sc := sc + 10, given := given + 10 goto Checking;
                                                        edge ptwenty do yc := yc - 20, sc := sc + 20, given := given + 20 goto Checking;

                                                    location Checking:
                                                        edge ask_more    when given <  45                                    goto Paying;
                                                        edge get_product when given >= 45 do ps := ps - 1, cha := given - 45 goto Getting;

                                                    location Getting:
                                                        edge deliver do sc := sc - cha, yc := yc + cha, given := 0, cha := 0 goto Paying;
                                                end

CIF model for example solution to exercise 6b:

                                                automaton market:
                                                    event pfive, pten, ptwenty, give_money, ask_more, get_product, deliver;
                                                    disc int yc = 225, sc = 0, ps = 5, given = 0, cha = 0, hand = 0;

                                                    location Paying:
                                                        initial;
                                                        edge pfive      do hand := hand + 5;
                                                        edge pten       do hand := hand + 10;
                                                        edge ptwenty    do hand := hand + 20;
                                                        edge give_money do yc := yc - hand, sc := sc + hand, given := given + hand, hand := 0 goto Checking;

                                                    location Checking:
                                                        edge ask_more    when given <  45                                    goto Paying;
                                                        edge get_product when given >= 45 do ps := ps - 1, cha := given - 45 goto Getting;

                                                    location Getting:
                                                        edge deliver do sc := sc - cha, yc := yc + cha, given := 0, cha := 0 goto Paying;
                                                end

7c: Using simulation of the example solutions, can you spot the problems in these models? And can you adapt the models to solve the problems? Hint: Think about negative values.

##

When you do not have money or the stock is empty, you can still pay and get a product. This means you borrowed money, which was stated in exercise 6 as not being allowed. And the salesman sold products he does not have.

You maybe did not notice this behavior when looking at the graphical representation of the automata. Thus, it is always wise to check the model's behavior using simulation.

For situation 1, we add guards `yc >= 5`, `yc >= 10` and `yc >= 20` to the edges with events `pfive`, `pten` and `ptwenty`, respectively. Furthermore, we add guard `ps > 0` to the same three edges, to prevent giving money to the salesman when he doesn't have any products left to sell.

                                                automaton market:
                                                    event pfive, pten, ptwenty, ask_more, get_product, deliver;
                                                    disc int yc = 225, sc = 0, ps = 5, given = 0, cha = 0;

                                                    location Paying:
                                                        initial;
                                                        edge pfive   when yc >= 5,  ps > 0 do yc := yc - 5,  sc := sc + 5,  given := given + 5  goto Checking;
                                                        edge pten    when yc >= 10, ps > 0 do yc := yc - 10, sc := sc + 10, given := given + 10 goto Checking;
                                                        edge ptwenty when yc >= 20, ps > 0 do yc := yc - 20, sc := sc + 20, given := given + 20 goto Checking;

                                                    location Checking:
                                                        edge ask_more    when given <  45                                    goto Paying;
                                                        edge get_product when given >= 45 do ps := ps - 1, cha := given - 45 goto Getting;

                                                    location Getting:
                                                        edge deliver do sc := sc - cha, yc := yc + cha, given := 0, cha := 0 goto Paying;
                                                end

For situation 2, we add `yc - hand >= 5`, `yc - hand >= 10` and `yc - hand >= 20` to the edges with events `pfive`, `pten` and `ptwenty`, respectively. Furthermore, we add guard `ps > 0` to the edge with the `give_money` event, to prevent giving money to the salesman when he doesn't have any products left to sell.

                                                automaton market:
                                                    event pfive, pten, ptwenty, give_money, ask_more, get_product, deliver;
                                                    disc int yc = 225, sc = 0, ps = 5, given = 0, cha = 0, hand = 0;

                                                    location Paying:
                                                        initial;
                                                        edge pfive   when yc - hand >= 5  do hand := hand + 5;
                                                        edge pten    when yc - hand >= 10 do hand := hand + 10;
                                                        edge ptwenty when yc - hand >= 20 do hand := hand + 20;
                                                        edge give_money when ps > 0 do yc := yc - hand, sc := sc + hand, given := given + hand, hand := 0 goto Checking;

                                                    location Checking:
                                                        edge ask_more    when given <  45                                    goto Paying;
                                                        edge get_product when given >= 45 do ps := ps - 1, cha := given - 45 goto Getting;

                                                    location Getting:
                                                        edge deliver do sc := sc - cha, yc := yc + cha, given := 0, cha := 0 goto Paying;
                                                end

## Exercise 8

Make CIF models of the example solutions of exercises 1 through 5 and check through simulation whether they are correct. If you have alternative solutions, also model those and check whether they exhibit the same behavior.

##

                                                automaton VendingMachine:
                                                    event give_coin, reject_coin, deliver;

                                                    location Waiting:
                                                        initial;
                                                        marked;
                                                        edge give_coin goto Busy;

                                                    location Busy:
                                                        edge give_coin goto Rejecting;
                                                        edge deliver goto Waiting;

                                                    location Rejecting:
                                                        edge reject_coin goto Busy;
                                                end

##

To avoid long lines, we split the event declarations over two declarations, one per line.

                                                automaton CoffeeMachine:
                                                    event make_choice, start_heating, add_water_to_beans, deliver;
                                                    event emergency, reset;

                                                    location Waiting:
                                                        initial;
                                                        marked;
                                                        edge make_choice goto Grinding;
                                                        edge emergency goto Emergency;

                                                    location Grinding:
                                                        edge start_heating goto Heating;
                                                        edge emergency goto Emergency;

                                                    location Heating:
                                                        edge add_water_to_beans goto Extracting;
                                                        edge emergency goto Emergency;

                                                    location Extracting:
                                                        edge deliver goto Waiting;
                                                        edge emergency goto Emergency;

                                                    location Emergency:
                                                        edge emergency;
                                                        edge reset goto Waiting;
                                                end

##

We put location `NotUsed` first. This way the initial location is listed first. It also keeps the other two locations, which are very similar, close to each other.

                                                automaton Bicycle:
                                                    event ride_A, ride_B, leave_A, leave_B;

                                                    location NotUsed:
                                                        initial;
                                                        marked;
                                                        edge ride_A goto RidingA;
                                                        edge ride_B goto RidingB;

                                                    location RidingA:
                                                        edge leave_A goto NotUsed;

                                                    location RidingB:
                                                        edge leave_B goto NotUsed;
                                                end

##

Names in CIF may not start with a digit, so we name the locations `Off0` and not `0Off`, and so on. We put the locations where the lamp is off first, as they are similar. The locations where the lamp is on are also similar, and they are at the end. We put the edges for `decrement` first in each edge, as they go to the previous location, making the model easier to read.

                                                automaton EvenLamp:
                                                    event increment, decrement, turn_on, turn_off;

                                                    location Off0:
                                                        initial;
                                                        marked;
                                                        edge increment goto Off1;
                                                        edge turn_on   goto On0;

                                                    location Off1:
                                                        edge decrement goto Off0;
                                                        edge increment goto Off2;

                                                    location Off2:
                                                        edge decrement goto Off1;
                                                        edge increment goto Off3;
                                                        edge turn_on   goto On2;

                                                    location Off3:
                                                        edge decrement goto Off2;
                                                        edge increment goto Off4;

                                                    location Off4:
                                                        edge decrement goto Off3;
                                                        edge turn_on   goto On4;

                                                    location On0:
                                                        edge turn_off  goto Off0;

                                                    location On2:
                                                        edge turn_off  goto Off2;

                                                    location On4:
                                                        edge turn_off  goto Off4;
                                                end

##

                                                automaton EvenLamp:
                                                    event increment, decrement, turn_on, turn_off;
                                                    disc int count = 0;
                                                    marked count = 0;

                                                    location Off:
                                                        initial;
                                                        marked;
                                                        edge decrement when count > 0 do count := count - 1;
                                                        edge increment when count < 4 do count := count + 1;
                                                        edge turn_on   when count mod 2 = 0 goto On;

                                                    location On:
                                                        edge turn_off  goto Off;
                                                end