Modelling and Verification 2009
Second Mini-project

Bureaucratic Information

Literature

Read A Tutorial on UPPAAL.

Second Mini-Project: Rush Hour

Before you start working on this mini-project, you should You are asked to provide a very brief report about how you solved the tasks below. There is no need to write any introduction or any additional text, just complete all the tasks below and copy and paste your implementations directly into the report. The report should be delivered as a PDF document.

Your tasks are as follows.

  1. 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.
  2. 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!
  3. 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.
  4. 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?
  5. 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.
  6. 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.
  7. Use (and describe) the resulting message sequence charts for illustrating the solutions.
  8. 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.
  9. Finish your report by briefly commenting on what was your experience working with the tool.
  10. Compile a single PDF file and post the file on the intranet by the stated deadline.