Second Mini-project

- The mini-project is supposed to be solved in groups of two or
three students and short reports should be posted on the intranet by
the stated deadline.
**Late submissions will not be accepted.** - The solutions of different groups must be independent and sharing
parts of the code or the text of the report is
**strictly forbidden**. - The mini-project will account for 30% of your final mark for the course.
- The deadline for delivering the second mini-project is Wednesday, 13 May, at 23:00.

- have read A Tutorial on UPPAAL, and
- have installed and can run Uppaal on your laptop.

Your tasks are as follows.

- Form a group of at most three students. Write the names and email addresses of all members of your group on the front page of your report.
- In this exercise you are asked to model the solitair game RUSH HOUR and solve use UPPAAL to solve the puzzle. The game is simple. You have a 6x6 board like shown on the picture to be found here. On the board you find a number of cars of different size (personal vehicles and trucks). The goal of the game is to move the cars 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!
- Make a model of the game in UPPAAL. Hint: you may want to model each (type of) car as an automaton (template), where a car can only move one position at a time. Also, you could use a doubly-indexed bit-array to represent information about locations on the board which are currently occupied.
- Using your model and the model checker of UPPAAL solve the two
puzzles shown in the picture here. What is
the
*shortest*number of steps/moves needed to solve the puzzle? - Extend your model with timing constraint. Assume that you have two hands, so that you potentially can move two cars (one position) simultaneously. Furthermore assume that you are left-handed so that it takes 3 seconds to move a car one position with the left hand but 5 seconds to move a car one position with the right hand.
- Use Uppaal to find the
*fastest*way of solving the puzzle (not measured in computation time, but in terms of the overall time that it takes to move all the cars). Tip: Use UPPAAL's diagnostic trace feature and ask for the fastest trace. - Use (and describe) the resulting message sequence charts for illustrating the solutions.
- Optional: Possibly also consider a timed model where each car has its own driver able to move his car one position within 3 seconds (trucks) or 2 seconds (personal vehicles). Thus several cars can move simultaneously. Again find the fastest solution.
- Finish your report by briefly commenting on what was your experience working with the tool.
- Compile a single PDF file and post the file on the intranet by the stated deadline.