Exercises for Dina Workshop

Exercises

A simple Coffee Machine

The purpose of this exercise is to familiarize you with the UppAal tool kit and to get a feeling for modelling of reactive systems.
The task is to model a simple coffee machine. Part of the job has already been done, because there is a system Coffemaker stored in the folder Dina in the UppAal tool. It is a simple finite state machine, which looks as follows:

1. Load the system and try a simulation to see that it actually goes through the motions.

2. Try checking the following properties with the verifier:

  a. A[] not deadlock
  b. A<> CoffeeMaker.coffee
  c. E<> CoffeeMaker.coffee
  d. CoffeeMaker.brew --> CoffeeMaker.coffee
  e. E<> CoffeeMaker.tea

3. Our coffee machine is sometimes a bit unpredictable and produces tea (thin coffee) and then refuses to move further. Add a transition (brew to tea) to this effect. And repeat the simulation and verification.

4. After complaints from our costumers, we manage to get the machine to return to idle, when tea has been brewed. Model this improved version.

5. The model is very abstract; it takes no resources to brew coffee. We want to model this by introducing state variables amount and oldamount. ( These have already been added to the global declarations). We now stipulate that at the transition from start, amount gets the initial value 50 (assignment amount := 50). Coffee costs 4 units (assignment amount := amount - 4). and tea costs 2 units. Modify the model and simulate it. What happens when amount becomes negative? Check the invariant A[] amount >= 0.

6. To really check amount, we use oldamount, and introduce a guard amount < oldamount on the transitions from coffee and tea to idle. We also need to assign oldamount := amount, just before brewing. Modify the model and recheck properties.

7. We should be able to resupply. When in idle, we should not brew unless amount >= 4, otherwise we should go to stop, and from there return to start. Remember to check properties! Perhaps it is a good idea also to check :

 A[] CoffeeMaker.stop imply amount <= 4.

8. It is still a bit strange that property 2.d does not hold in the weaker form:

  CoffeeMaker.brew --> CoffeeMaker.coffee or CoffeeMaker.tea

We need to limit the duration of brewing. Introduce a clock c in the global declarations, reset it before brewing and give brew an invariant c < 10.

9. We have a similar problem with 2 b (in a weaker form). Try committing the states that should take no time. until the property:

  A<> CoffeeMaker.coffee or CoffeeMaker.tea

holds.

10. What about guards that ensure proper brewing: c > 8 for coffee and c > 15 for tea? Check the properties!

We have completed building a coffee machine.

The Coffee Vending Machine

We have success with our coffee machine, so we want payment for each cup of coffee. We buy a MoneyBox from an independent vendor., it has a dangling wire (a channel), so we make it a Box connected to a channel link. See the system VendingMachine.

1. Check the properties! Suddenly there seems to be a problem with an infinite loop in the Box. Please repair it by inserting a delay!

2. Synchronize the money box and the CoffeeMaker; it should start to brew on an ok signal. There is a problem, the system deadlocks, because idle can no longer be committed; but it can be urgent. What is the difference?

3. Modify the MoneyBox so it has a local counter amount which counts the number of good coins. You can find a solution as VendingMachine1.

4. Make a new template representing a toggle switch. It should change a boolean parameter X between 0 and 1, whenever it receives a signal on a channel parameter toggle. A solution is found in Toggle

5. Modify the Vending Machine such that it instantiates a toggle with a channel switch and a variable COFFEE. Remember to check properties.

6. Modify the coffee machine so it makes tea when COFFEE == 0 or otherwise coffee. Check the properties.

7. Modify the MoneyBox so it first start when it gets a signal on a coin channel. Declare such a global channel and introduce a user process that first flips the switch a number of times and then drops a coin. Check the properties! The system is in VendingMachine_final.

Building Models

For the remaining part of the exercises, we suggest that you get together according to preferences and try to model aspects of either the API control [BBR02] or the T-cell. [KCH01].