Formal Modelling and Analysis of Real-Time Systems: Lab 3
Part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'04.
Exercise: Vector Rally
In this exercise you are asked to model and analyse an optimisation
problem, proposed by Kåre J. Kristoffersen in 2003.
The purpose of Vector Rally is to simulate the challenges met when
driving a vehicle as fast as possible through a course with many
turns and obstacles. It is natural in the sense that it involves
acceleration, and captures nicely the fact that one needs to slow
down before taking a turn. The purpose of the challenge is to use a
model-checker to find the optimal path (i.e. the fastest/shortest path)
on a rally course.
An example of a rally course is shown in this figure:
The vehicle is represented by the two integer pairs position =
(x, y) and speed = (dx,dy). In each step the vehicle
changes position by adding speed to position (i.e. the
next position is (dx+x,dy+y)) possibly by first adjusting speed
by +/- 1 horizontally and/or vertically.
The vehicle starts in position (0,0) with speed (0,0). It should
reach the goal (represented by a vertical or horizontal line), but
without going out of bound as well as hitting or crossing any of the
obstacles. In the figure above, a vector from (5,6) to (8,6) is
illegal (the vector from (5,6) to (8,8) or (7,8) are also illegal).