Project is based on B Specification for Spaceship & Asteroids game.
The Spaceship can traverse in a grid space of 12x7 and some specific locations of the space are populated with asteroids. User is given the Starbase position which is the Spaceship's destination where the spaceship should be docked.
Initially Spaceship is in Homebase(1,1) with 100 units of power and each movement costs power and user should get the Spaceship to the Starbase before the power runs out to win the game.
Each movement and asteroid crash reduces Spaceship's power,
Nomral Movement -> 5 units of power
Warp Jump -> 20 units of power
Crash into Asteroid -> 10 units of power
- Spaceship is docked at the Starbase -> Game Won
- Spaceship is not docked at the Starbase & No power for movement -> Game Lost
- Otherwise -> Game Not Over
Machine was implemented with operations for the movement of the spaceship, warp jump, New Game/Reset Game, Mission Status, Visited Regions, Docked at Starbase and Game Status.
- Atelier B
- ProB
ProB tool configurations
Preferences -> Configurations -> MININT..MAXINT (32bit)
Preferences -> Animation preferences -> MAX_OPERATIONS (Set MAX_OPERATIONS > 100)
Athindu Umayanga : @Athindu
The project was developed to complete the coursework in Reasoning about Programs module at University of Westminster.