# Modelling Exercises

Choose one of the five exercises below. Your solution should contain two parts, a main part containing in a documented fashion the modeling and analyses of the particular system you have chosen using UPPAAL 4.0 (see www.uppaal.com).  Also your solution should ideally contain a shorter secondary part possibly addressing

• ideas for possible future modellering patterns,
• suggestions for extensions of UPPAAL (syntactically, functionally), and/or
• evaluation of UPPAAL,
• ...

You may hand in solutions in groups with at most 3 persons. The solution should be some 5-10 typeset pages. The complete report should be delivered on

• Monday, March 26 (at noon)

## Exercise 1 (Elevator system)

Model and analyze a control system of an elevator-system of your own design serving a number of floors (say 4 or 5) and with a number of lifts (say 2 or 3) and with a number of users being on individual floors and with individual wishes for getting to different floors. The system may:

• allow the user may  indicate that a lift is required at a certain floor, and/or needs to go up or down and/or is requested to go to a certain floor
• or the user may -- once inside the lift -- request actual floor.
• In order to move the doors must be closed.
• floors cannot be skiped.
• The initial position of all the lifts is floor 1. a The elevator is controlled by only one button by which it is possible to order the elevator to the floor where you stand.

In modelling the elevator system itself assumption of the time to get from one floor to another. Also model timing assumptions as to the arrivial of users of the elevator system.  Try to validate various safety and progress properties that you may want the system to satisfy.

## Exercise 2 (Leader Election Protocol)

In this exercise you will consider a simple leader election protocol. The setting is the following: There are a number of interconnected network nodes. Each node has an address. The goal of the protocol is to identify the node with the lowest address is the network and elect that node to be the leader. In order to be correct, all connected nodes should have elected the same leader.

As part of the protocol, each node maintains information about which node it thinks is the leader and the number of hops (network links) to the leader. Let's say that the information at node i is stored as a pair ni=(l, h). It is perfectly valid for a node to believe that itself is the leader and in this case the number of hops to the leader is 0, e.g. n1=(1,0).

The protocol transmits messages on the form m=(source, destination, leader, hops) between the nodes. Here source is the address of the node sending the message, destination is the address of the node receiving the message, leader is information about which node source thinks is the leader and hops is the number of hops (network links) between the source and the leader.

Whenever ni is updated, node i sends a message m=(i, d, ni.leader, ni.hops) to each of its neighbours d, with the exception that it does not send a message back to the source of message which triggered the update in the first place. There is an upper time bound on the arrival of the message called MSG_DELAY. Notice that there is no lower bound on the delivery and that messages might be reordered.

The final ingredient of the protocol is a timeout mechanism. If a node has not receive any messages, except those which are discarded, for more than a certain timeout period, then a timeout will happen within TIMEOUT_DELAY time units (i.e. there is a reaction delay) -- this means that there is actually a range of ]timeout; timeout+TIMEOUT_DELAY] after the last receiption of a "good" message in which a timeout will happen. Initially, the timeout is a constant INITIAL_TIMEOUT. When receiving good messages (messages which do not contain worse information than what we already got), then the timeout is set to INITIAL_TIMEOUT + TIMEOUT_DELAY + ni.hops * MESSAGE_DELAY. When a node times out, it will elect itself as the new leader and send an update message to all its neighbors.

• model an instance of the above protocol with three connected nodes (e.g. a fully connected topology - this might be the simplest to model) and the following constants:  Constant Value INITIAL_TIMEOUT 10 TIMEOUT_DELAY 5 MESSAGE_DELAY 3
• use the simulator to convince yourself that it works as intended,
• verify that it is possible for the system to come in a state, where all nodes know the correct leader
• verify that a it is always the case that a node i knows the correct leader after TIMEOUT + TIMEOUT_DELAY + DISTANCEi * MSG_DELAY, where DISTANCEi is the real number of hops from i to the correct leader.

Notice that you should not model topology changes (network links appearing or disappearing).

A few tips for your modeling work:

• Make a node template for modeling a node. Instantiate it once for each node of the network.
• Make a message template, which is used to represent a message. You will need a number of instances of this template. For 3 nodes, 10 should suffice. Use the model checker to verify that you do indeed have enough message processes.
• You can use shared variables and channels for the communication between the node processes and the message processes.
• Initially, before any messages are sent, each node believes it is the leader (like in the first figure).

## Exercise 4 (Rush Hour)

In this exercise you are asked to model a solitaire game and use UPPAAL to solve the puzzle. The game is simple. You have a 6x6 board as shown on the picture below. On the board you find a number of cars of different sizes (personal vehicles and trucks). The goal of the game is to move the cars and trucks by driving forward and backwards in such a way that the RED car can leave the board at the exit on the right side of the board. The cars cannot turn!

• Task 1: Make a model of the game in UPPAAL. Obviously you model should allow for different puzzles to be dealt with.
• Task 2: Use your model to solve the two puzzles (no. 13 and 21) shown in he second picture. What is the shortest number of steps/moves needed to solve the puzzle?
• Task 3: Extend your model with timing constraint. Assume that it takes a different amount of time to move the cars, e.g. 2 time units for the small ones and 3 for the trucks (you can also choose to give each car its own time). Try to experiment with different assumptions as to the number of hands  / drivers, i.e. how many cars that can move at the same time.
• Task 4: Use Uppaal to find the fastest way of solving the puzzle (not measured in computation time, but in time it take to move all the cars). Tip: Use Uppaals diagnostic trace feature and ask for the fastest trace.

Special challenge: you may want to deal with the more challenging RAILROAD Rush Hour, which is on a 7x7 boards and with 2x2 blockers that can move bort horizontal and vertical (see figure below).  Again the objective is to get the RED train out of the exit (to the right).

## Exercise 5 (Crossing the River)

Help a familly shown below to cross a river according to the following constraints (click on the picture or here to activate an interactive version of this puzzle):
• Max 2 persons on the boat,
• Mom not alone with boys,
• Dad ont alone with girls,
• Thief not alone with family,
• Only police officer, dad and mom can handle the boat.
• Task 1: Make an Uppaal model of it and generate a feasible schedule.
• Task 2: Add temporal constraints (e.g. each adult take a certain time to cross the river with the boat) and try to find the quickest possible schedule.
• Task 3: Determine the feasibility limit depending on the number of boys, girls, prisonners.
• Task 4: Try other parameters and constraints for this game.