This coursework requires you to develop a B specification of a very simple version of the old

Asteroids arcade game, using the B tools Atelier B & ProB.

Figure $1.$ gives the layout of the regions of space $($a rectangular grid shape$),$ the Spaceship is

represented by the blue triangle, its starting position is its home base $(1,1).$

The aim is to move the Spaceship from its home base through space using the various movement

operations to get to the Starbase $(6,4),$ avoiding the Asteroids.

Figure $1.$ Regions of Space, Spaceship, Star Base & Asteroids

Notes

$$ Space is made up of regions $($squares of the grid$)12$ wide by $7$ high.

$$ The regions of space are populated by $11$ asteroids, each in one region of space, and

located as shown in Figure $1.$

$$ The Spaceship occupies only one square at a time which must be either an "empty space

square" or the Starbase in its square $(6,4).$

For example, the Spaceship can be in region $(5,3),$ but not $(8,3)$ as it is occupied by an

asteroid.

$$ The Spaceship is initially in its homebase, i$.$e$.$ the bottom left square $(1,1).$

$$ The spaceship can make a normal move, i$.$e$.$ from one region of space $($grid square$)$ to an

adjacent one, in one of four directions: Up$,$ Down, Left and Right.

$$ It uses up $5$ units of power when it makes a normal move.

$$ The spaceship can engage its warp$-$drive to $$jump$$ to any region of space, except one

occupied by an asteroid. It must not travel outside known space, i$.$e$.$ outside the grid.

$$ It uses up $20$ units of power when it engages its warp$-$drive, no matter how far it moves.

$$ If the spaceship crashes into one of the asteroids it loses $10$ units of power and bounces

back into the square it came from.

$$ It cannot do a move for which it does not have the required amount of power.

$$ The state of the game is one of the following:

$$ the spaceship docks at the Starbase, in which case the game has been Won.

$$ the spaceship is not docked at the Starbase & can not move because it has run out

of power, in which case the game is Lost.

$$ otherwise the game is not over.

$2$ Develop a B Specification of the Regions of Space, Spaceship & Asteroids

Your B specification, i$.$e$.$ collection of one or more B machines, should include the following elements.

$2\mathrm{.}1$ Sets and Constants

Any sets and constants that are required to define the data and state of the spaceship, space,

asteroids and their properties.

$($Hints: Represent space and the asteroids as relations. What is the relationship between space,

"empty space" & the asteroids locations?$)$

$2\mathrm{.}2$ System State

The state variables required to represent space, asteroids and the spaceship. Including the state

invariant and initialisation.

You can assume that the spaceship starts at its homebase, has no power yet, has not had any

collisions and it has only visited the regions of space its homebase is located in$.$

$2\mathrm{.}3$ New Game

To start or re$-$start the game use the NewGame$($ power $)$ operation. This should reset the spaceship

to the initial state, except that it sets its power level to the value of the power parameter.

$2\mathrm{.}4$ Spaceship Movements in Space

Note that all movement operations must report the outcome of an attempted movement. That is$,$

either it was successful, failed due to space boundary issues, failed due to an asteroid, or failed for

some other reason.

$2\mathrm{.}4\mathrm{.}1$ Normal Spaceship Movements

The following operations are the basic movements that all move the spaceship one region $($square$)$ in

the appropriate direction in space and uses up $5$ units of the spaceship's power:

$$ MoveUp

$$ MoveDown

$$ MoveLeft

$$ MoveRight

Note that If the move results in the spaceship hitting an asteroid the spaceship remains in its current

location, but its power is reduced by $10$ units.

If any attempted movement cannot be performed because of the boundary of space or insufficient

power then an error is reported.

$2\mathrm{.}4\mathrm{.}2$ Warp$-$drive Spaceship Movement

The movement operation:

$$ WarpDrive$($ newposition $)$

where the player enters the newposition parameter, the region of space $($i$.$e$.$ grid co$-$ordinates$)$ that

the spaceship should warp jump to$.$ Engaging the warp$-$drive uses up $20$ units of the spaceship's

power.

If the warp$-$drive cannot be used because the destination region input is either not within the known

regions of space or is occupied by an asteroid or if there is insufficient power to use the warp$-$drive

then an appropriate error message should be reported.

$2\mathrm{.}5$ Spaceship's Mission Status

An enquiry operation MissionStatus that reports the current status of the spaceship:

$$ the game status $($WON$,$ LOST, or NOT$\_$OVER$),$

$$ its current location,

$$ its current power reserves,

$$ how many asteroid collisions it has had.

$2\mathrm{.}6$ Spaceship's Mission Route

An enquiry operation RegionsVisited that reports the regions of space that the spaceship has

travelled through.

$2\mathrm{.}8$ General Requirements

The B specification should use the appropriate features to define the data and operations in your B

machine.

The specification must be syntactically and type correct, as checked by using the Atelier B tool.