Modelling and Verification 2009
- 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
- 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.
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.
- 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.