Coursework Description 1. Introduction This coursework requires you to develop a B specification of a very simple version of the old Spaceship & Asteroids arcade game, using the B tools Atelier B &...

1 answer below »
Coursework Description 1. Introduction This coursework requires you to develop a B specification of a very simple version of the old Spaceship & 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, & located as shown in Figure 1.  The Spaceship occupies only one square at a time & can only be in an "empty space square", except when “docked” at 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, Forward (right) & Reverse (left).  It uses up 5 units of power when it makes a normal move.  The spaceship can engage its warp-drive & "jumps" 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 many regions it moves.  If the spaceship crashes into one of the asteroids it loses 10 units of power.  If it has less than the required amount of power to do either a normal move or a warp-drive jump it can not do that type of move. 6SENG001W Coursework 1 3 17/10/2021  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 1 or more B machines, should include the following elements. 2.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.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, has not had any collisions and it has only visited the regions of space its homebase is located in. 2.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.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.4.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  MoveForward  MoveBackward (i.e. reverse) 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. 6SENG001W Coursework 1 4 17/10/2021 2.4.2 Warp-drive Spaceship Movement The movement operation:  EngageWarpDrive( 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.5 Spaceship's Mission Status An enquiry operation MissionStatus that reports the current status of the spaceship:  its current location,  its current power reserves,  how many asteroid collisions it has had. 2.6 Spaceship's Mission Route An enquiry operation RegionsVisited that reports the regions of space that the spaceship has travelled through. 2.7 Spaceship is Docked at Starbase An enquiry operation DockedAtStarbase that reports whether the Spaceship is “docked” at the Starbase, i.e. its current location is the Starbase. 2.7 Game Status An enquiry operation GameStatus that reports:  "Game WON" if the game is over & has been won;  "Game LOST" if over & has been lost; and  "Game Not Over" if its not over. 2.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. The specification must be animated by ProB. That is it must initialise correctly and all operations can be animated successfully and used to move the Spaceship around the regions of space, e.g. from the homebase to the Starbase using a combination of all of the movement operations, including the warp jump. 6SENG001W Coursework 1 5 17/10/2021 3. Submission & Lab Demonstration 3.1 Blackboard Submission The following 3 components are to be submitted via Blackboard: 1. The Structure Diagram of your Spaceship & Asteroids System B machine. You must also include as a "plain English" description of the "state invariants" of the system. Examples of Structure Diagrams can be found in the lecture notes and in the tutorial exercises. SUBMIT: 1 ".pdf" file. [15%] 2. The B Specification of the Spaceship & Asteroids System. SUBMIT: the B machine ".mch" file as is. (DO NOT submit it as a Word file.) [70%] 3. Examples of successfully using the 2 B tools Atelier B and Prob. For Atelier B: a single screen shot showing the B specification in the Atelier B editor and in Atelier B's main window the successful type checking of the specification, i.e. the “specification box” with the “green TC” circle. For ProB: a Graph representation of a complete ProB Animation Session history. Using ProB perform an animation sessions that shows how the Spaceship is moved from the homebase square to the Starbase square using a combination of all of the movement operations, including examples of non-successful operations. Notes the submitted example animation should not just consist of a single warp from the homebase to the Starbase. View this Animation Session as a "DOT" graph and then save it. SUBMIT:  1 Atelier B screen shot in either “.jpg” or “.jpeg” format.  1 ProB animation history graph ".dot" file as is. (DO NOT open using Word.) [15%] NOTE: All files should be compressed into a single ZIP archive. ONLY ZIP format archives will be accepted.
Answered 5 days AfterOct 23, 2021

Answer To: Coursework Description 1. Introduction This coursework requires you to develop a B specification of...

Amar Kumar answered on Oct 29 2021
111 Votes
spaceship/graphical-view.png
spaceship/README.md
# Spaceship & Asteroids arcade game - B specification
B specification of a very simple version of the old Spaceship & Asteroids arcade game, using the B tools: Atelier B & ProB.
Uses the following machines:
* [`Space`](reasoning_cw/reasoning_cw/Space.mch)
* [`SpaceShip`](reasoning_cw/reasoning_cw/SpaceShip.mch)
Features a graphical view, which uses an animation function. Images used by the animation function are in [this](reasoning_cw/reasoning_cw/images) directory.
![Graphical view](./graphical-view.png)
spaceship/reasoning_cw/reasoning_cw.desc
C:\Users\senth\Desktop\reasoning_cw\reasoning_cw\bdp
C:\Users\senth\Desktop\reasoning_cw\reasoning_cw\lang
senth

spaceship/reasoning_cw/reasoning_cw/bdp/.lib
spaceship/reasoning_cw/reasoning_cw/bdp/.project
spaceship/reasoning_cw/reasoning_cw/bdp/AtelierB
ATB*ATB*Encoding:UTF-8
ATB*POG*Generate_Obvious_PO:FALSE
ATB*POG*Generate_WD_PO:TRUE
ATB*ATB*Proof_Obligations_Generator_NG:TRUE
ATB*PR*Use_Rule_Package:?
spaceship/reasoning_cw/reasoning_cw/bdp/expand_src/Space.mch
/* Space
* Author: Senthuran Ambalavanar | 2015215 | w1608452
* Creation date: 24/11/2018
*/
MACHINE
Space
CONCRETE_CONSTANTS
spaceX , spaceY , space , asteroids , emptySpace , homeBase , starBase
PROPERTIES
// The known space
spaceX = 1 .. 12 &
spaceY = 1 .. 7 &
space = spaceX * spaceY &
// Asteroids
asteroids <: space &
asteroids = { 3 |-> 2 , 3 |-> 5 , 5 |-> 4 , 6 |-> 7 , 7 |-> 1 , 7 |-> 5 , 7 |-> 7 , 8 |-> 3 , 10 |-> 6 , 11 |-> 2 , 12 |-> 5 } &
// Empty Space
emptySpace <: space &
emptySpace /\ asteroids = {} &
emptySpace \/ asteroids = space &
// Home base and Star Base
homeBase : emptySpace & homeBase = 1 |-> 1 &
starBase : emptySpace & starBase = 6 |-> 4
END
spaceship/reasoning_cw/reasoning_cw/bdp/expand_src/SpaceShip.mch
/* SpaceShip
* Author: Senthuran Ambalavanar | 2015215 | w1608452
* Creation date: 24/11/2018
*/
MACHINE
SpaceShip
SEES
Space
SETS
REPORT = { SUCCESSFULLY_MOVED , CANNOT_MOVE_OUT_OF_KNOWN_SPACE , INSUFFICIENT_POWER , HIT_ASTEROID , CANNOT_WARP_INTO_ASTEROID , CANNOT_WARP_TO_THE_SAME_POSITION , CANNOT_IMMEDIATELY_WARP_INTO_STARBASE } ;
MOVEMENT = { MOVE_UP , MOVE_DOWN , MOVE_FORWARD , MOVE_BACKWARD , WARP } ;
DOCKED_STATUS = { YES , NO } ;
GAME_STATUS = { GAME_WON , GAME_LOST , GAME_NOT_OVER }
CONCRETE_CONSTANTS
normalMovePower , warpDrivePower , asteroidHitPowerLoss , initialPower
PROPERTIES
normalMovePower = 5 &
warpDrivePower = 20 &
asteroidHitPowerLoss = 10 &
initialPower = 100
DEFINITIONS
isWithinSpace ( xx , yy ) == ( xx |-> yy : space ) ;
isHitAsteroid ( xx , yy ) == ( xx |-> yy : asteroids ) ;
hasEnoughPower ( cp , rp ) == ( cp >= rp ) ;
isDocked == ( xPosition |-> yPosition = starBase ) ;
isGameFinished == isDocked or ( power < normalMovePower ) ;
ANIMATION_FUNCTION == ( { rr , cc , ii | rr : spaceY & cc : spaceX &
( IF ( cc = prj1 ( spaceX , spaceY ) ( starBase ) & rr = prj2 ( spaceX , spaceY ) ( starBase ) )
THEN
// Star base
ii = 3
ELSE
IF ( cc |-> ( 8 - rr ) : asteroids )
THEN
// Asteroid
ii = 1
ELSE
IF ( cc = xPosition & rr = ( 8 - yPosition ) )
THEN
// Spaceship
ii = 2
ELSE
// Empty space
ii = 0
END
END
END ) } ) ;
ANIMATION_IMG0 == "images/empty.gif" ;
ANIMATION_IMG1 == "images/asteroid.gif" ;
ANIMATION_IMG2 == "images/spaceship.gif" ;
ANIMATION_IMG3 == "images/starbase.gif" ;
ABSTRACT_VARIABLES
xPosition , yPosition , power , noOfCollisions , takenRoute , movements
INVARIANT
xPosition : spaceX &
yPosition : spaceY &
xPosition |-> yP
osition : emptySpace &
power : NAT &
noOfCollisions : NAT &
takenRoute : seq ( emptySpace ) &
movements : seq ( MOVEMENT )
INITIALISATION
power := initialPower ||
noOfCollisions := 0 ||
xPosition := prj1 ( spaceX , spaceY ) ( homeBase ) ||
yPosition := prj2 ( spaceX , spaceY ) ( homeBase ) ||
takenRoute := [ homeBase ] ||
movements := []
OPERATIONS
/** Moves Up **/
report , movement <-- MoveUp =
PRE
report : REPORT & movement : MOVEMENT & not ( isGameFinished )
THEN
IF
hasEnoughPower ( power , normalMovePower )
THEN
IF
isWithinSpace ( xPosition , yPosition + 1 )
THEN
IF
not ( isHitAsteroid ( xPosition , yPosition + 1 ) )
THEN
IF
( power - normalMovePower >= 0 )
THEN
yPosition := yPosition + 1 ||
power := power - normalMovePower ||
takenRoute := takenRoute <- ( xPosition |-> yPosition + 1 ) ||
movements := movements <- MOVE_UP ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_UP
ELSE
// Prevents power going below 0
yPosition := yPosition + 1 ||
power := 0 ||
takenRoute := takenRoute <- ( xPosition |-> yPosition + 1 ) ||
movements := movements <- MOVE_UP ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_UP
END
ELSE
IF
( power - normalMovePower - asteroidHitPowerLoss >= 0 )
THEN
power := power - normalMovePower - asteroidHitPowerLoss ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_UP
ELSE
// Prevents power going below 0
power := 0 ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_UP
END
END
ELSE
report := CANNOT_MOVE_OUT_OF_KNOWN_SPACE
END
ELSE
report := INSUFFICIENT_POWER
END
END ;
/** Moves Down **/
report , movement <-- MoveDown =
PRE
report : REPORT & movement : MOVEMENT & not ( isGameFinished )
THEN
IF
hasEnoughPower ( power , normalMovePower )
THEN
IF
isWithinSpace ( xPosition , yPosition - 1 )
THEN
IF
not ( isHitAsteroid ( xPosition , yPosition - 1 ) )
THEN
IF
( power - normalMovePower >= 0 )
THEN
yPosition := yPosition - 1 ||
power := power - normalMovePower ||
takenRoute := takenRoute <- ( xPosition |-> yPosition - 1 ) ||
movements := movements <- MOVE_DOWN ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_DOWN
ELSE
// Prevents power going below 0
yPosition := yPosition - 1 ||
power := 0 ||
takenRoute := takenRoute <- ( xPosition |-> yPosition - 1 ) ||
movements := movements <- MOVE_DOWN ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_DOWN
END
ELSE
IF
( power - normalMovePower - asteroidHitPowerLoss >= 0 )
THEN
power := power - normalMovePower - asteroidHitPowerLoss ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_DOWN
ELSE
// Prevents power going below 0
power := 0 ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_DOWN
END
END
ELSE
report := CANNOT_MOVE_OUT_OF_KNOWN_SPACE
END
ELSE
report := INSUFFICIENT_POWER
END
END ;
/** Moves Forward (Right) **/
report , movement <-- MoveForward =
PRE
report : REPORT & movement : MOVEMENT & not ( isGameFinished )
THEN
IF
hasEnoughPower ( power , normalMovePower )
THEN
IF
isWithinSpace ( xPosition + 1 , yPosition )
THEN
IF
not ( isHitAsteroid ( xPosition + 1 , yPosition ) )
THEN
IF
( power - normalMovePower >= 0 )
THEN
xPosition := xPosition + 1 ||
power := power - normalMovePower ||
takenRoute := takenRoute <- ( xPosition + 1 |-> yPosition ) ||
movements := movements <- MOVE_FORWARD ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_FORWARD
ELSE
// Prevents power going below 0
xPosition := xPosition + 1 ||
power := 0 ||
takenRoute := takenRoute <- ( xPosition + 1 |-> yPosition ) ||
movements := movements <- MOVE_FORWARD ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_FORWARD
END
ELSE
IF
( power - normalMovePower - asteroidHitPowerLoss >= 0 )
THEN
power := power - normalMovePower - asteroidHitPowerLoss ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_FORWARD
ELSE
// Prevents power going below 0
power := 0 ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_FORWARD
END
END
ELSE
report := CANNOT_MOVE_OUT_OF_KNOWN_SPACE
END
ELSE
report := INSUFFICIENT_POWER
END
END ;
/** Moves Backward (Left) **/
report , movement <-- MoveBackward =
PRE
report : REPORT & movement : MOVEMENT & not ( isGameFinished )
THEN
IF
hasEnoughPower ( power , normalMovePower )
THEN
IF
isWithinSpace ( xPosition - 1 , yPosition )
THEN
IF
not ( isHitAsteroid ( xPosition - 1 , yPosition ) )
THEN
IF
( power - normalMovePower >= 0 )
THEN
xPosition := xPosition - 1 ||
power := power - normalMovePower ||
takenRoute := takenRoute <- ( xPosition - 1 |-> yPosition ) ||
movements := movements <- MOVE_BACKWARD ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_BACKWARD
ELSE
// Prevents power going below 0
xPosition := xPosition - 1 ||
power := 0 ||
takenRoute := takenRoute <- ( xPosition - 1 |-> yPosition ) ||
movements := movements <- MOVE_BACKWARD ||
report := SUCCESSFULLY_MOVED ||
movement := MOVE_BACKWARD
END
ELSE
IF
( power - normalMovePower - asteroidHitPowerLoss >= 0 )
THEN
power := power - normalMovePower - asteroidHitPowerLoss ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_BACKWARD
ELSE
// Prevents power going below 0
power := 0 ||
noOfCollisions := noOfCollisions + 1 ||
report := HIT_ASTEROID ||
movement := MOVE_BACKWARD
END
END
ELSE
report := CANNOT_MOVE_OUT_OF_KNOWN_SPACE
END
ELSE
report := INSUFFICIENT_POWER
END
END ;
/** Performs Warp Drive to the given position **/
report , movement <-- EngageWarpDrive ( newXPosition , newYPosition ) =
PRE
report : REPORT & movement : MOVEMENT &
newXPosition : NAT1 & newYPosition : NAT1 &
not ( isGameFinished )
THEN
IF
hasEnoughPower ( power , warpDrivePower )
THEN
IF
isWithinSpace ( newXPosition , newYPosition )
THEN
IF
( newXPosition = xPosition & newYPosition = yPosition )
THEN
report := CANNOT_WARP_TO_THE_SAME_POSITION
ELSE
IF
( size ( takenRoute ) = 1 & newXPosition |-> newYPosition = starBase )
THEN
report := CANNOT_IMMEDIATELY_WARP_INTO_STARBASE
ELSE
IF
not ( isHitAsteroid ( newXPosition , newYPosition ) )
THEN
IF
( power - warpDrivePower >= 0 )
THEN
power := power - warpDrivePower ||
xPosition := newXPosition ||
yPosition := newYPosition ||
takenRoute := takenRoute <- ( newXPosition |-> newYPosition ) ||
movements := movements <- WARP ||
report := SUCCESSFULLY_MOVED ||
movement := WARP
ELSE
// Prevents power going below 0
power := 0 ||
xPosition := newXPosition ||
yPosition := newYPosition ||
takenRoute := takenRoute <- ( newXPosition |-> newYPosition ) ||
movements := movements <- WARP ||
report := SUCCESSFULLY_MOVED ||
movement := WARP
END
ELSE
report := CANNOT_WARP_INTO_ASTEROID
END
END
END
ELSE
report := CANNOT_MOVE_OUT_OF_KNOWN_SPACE
END
ELSE
report := INSUFFICIENT_POWER
END
END ;
/** Gives the current status of the space ship **/
currentLocation , currentPower , asteroidCollisions <-- MissionStatus =
BEGIN
currentLocation := xPosition |-> yPosition ||
currentPower := power ||
asteroidCollisions := noOfCollisions
END ;
/** Gives the route that the space ship has travelled through **/
route <-- MissionRoute =
BEGIN
route := takenRoute
END ;
/** Reports whether the space ship is docked at the star base **/
dockedStatus <-- DockedAtStarbase =
PRE
dockedStatus : DOCKED_STATUS
THEN
IF
( isDocked )
THEN
dockedStatus := YES
ELSE
dockedStatus := NO
END
END ;
/** Reports the game status **/
status <-- GameStatus =
PRE
status : GAME_STATUS
THEN
IF
( isDocked )
THEN
status := GAME_WON
ELSE
IF
( power < normalMovePower )
THEN
status := GAME_LOST
ELSE
status := GAME_NOT_OVER
END
END
END ;
/** Reports the game status (as a string) **/
// status <-- GameStatus =
// IF
// (isDocked)
// THEN
// status := "Game WON"
// ELSE
// IF
// (power < normalMovePower)
// THEN
// status := "Game LOST"
// ELSE
// status := "Game Not Over"
// END
// END;
/** Gives all movements taken by the space ship **/
allMovements <-- takenMovements =
BEGIN
allMovements := movements
END ;
/** Resets the game, and starts again from the beginning **/
resetGame =
PRE
isGameFinished
THEN
power := initialPower ||
noOfCollisions := 0 ||
xPosition := prj1 ( spaceX , spaceY ) ( homeBase ) ||
yPosition := prj2 ( spaceX , spaceY ) ( homeBase ) ||
takenRoute := [ homeBase ] ||
movements := []
END
END
spaceship/reasoning_cw/reasoning_cw/bdp/MANIFEST
spaceship/reasoning_cw/reasoning_cw/bdp/reasoning_cw.db












spaceship/reasoning_cw/reasoning_cw/bdp/reasoning_cw.dot
digraph {
Space [ label=" Space " shape= box ]
SpaceShip [ label=" SpaceShip " shape= box ]
"SpaceShip" -> "Space" [style= dotted ]
}
spaceship/reasoning_cw/reasoning_cw/bdp/reasoning_cw.lib
spaceship/reasoning_cw/reasoning_cw/bdp/Space.chk
2db44628983c9fe65355a832d8097ba4
spaceship/reasoning_cw/reasoning_cw/bdp/Space.dep
file:24e1cc5165421596d3845313452298d2
spaceship/reasoning_cw/reasoning_cw/bdp/Space.nf
Normalised(
THEORY MagicNumberX IS
MagicNumber(Machine(Space))==(3.5)
END
&
THEORY UpperLevelX IS
First_Level(Machine(Space))==(Machine(Space));
Level(Machine(Space))==(0)
END
&
THEORY LoadedStructureX IS
Machine(Space)
END
&
THEORY ListSeesX IS
List_Sees(Machine(Space))==(?)
END
&
THEORY ListUsesX IS
List_Uses(Machine(Space))==(?)
END
&
THEORY ListIncludesX IS
Inherited_List_Includes(Machine(Space))==(?);
List_Includes(Machine(Space))==(?)
END
&
THEORY ListPromotesX IS
List_Promotes(Machine(Space))==(?)
END
&
THEORY ListExtendsX IS
List_Extends(Machine(Space))==(?)
END
&
THEORY ListVariablesX IS
External_Context_List_Variables(Machine(Space))==(?);
Context_List_Variables(Machine(Space))==(?);
Abstract_List_Variables(Machine(Space))==(?);
Local_List_Variables(Machine(Space))==(?);
List_Variables(Machine(Space))==(?);
External_List_Variables(Machine(Space))==(?)
END
&
THEORY ListVisibleVariablesX IS
Inherited_List_VisibleVariables(Machine(Space))==(?);
Abstract_List_VisibleVariables(Machine(Space))==(?);
External_List_VisibleVariables(Machine(Space))==(?);
Expanded_List_VisibleVariables(Machine(Space))==(?);
List_VisibleVariables(Machine(Space))==(?);
Internal_List_VisibleVariables(Machine(Space))==(?)
END
&
THEORY ListInvariantX IS
Gluing_Seen_List_Invariant(Machine(Space))==(btrue);
Gluing_List_Invariant(Machine(Space))==(btrue);
Expanded_List_Invariant(Machine(Space))==(btrue);
Abstract_List_Invariant(Machine(Space))==(btrue);
Context_List_Invariant(Machine(Space))==(btrue);
List_Invariant(Machine(Space))==(btrue)
END
&
THEORY ListAssertionsX IS
Expanded_List_Assertions(Machine(Space))==(btrue);
Abstract_List_Assertions(Machine(Space))==(btrue);
Context_List_Assertions(Machine(Space))==(btrue);
List_Assertions(Machine(Space))==(btrue)
END
&
THEORY ListCoverageX IS
List_Coverage(Machine(Space))==(btrue)
END
&
THEORY ListExclusivityX IS
List_Exclusivity(Machine(Space))==(btrue)
END
&
THEORY ListInitialisationX IS
Expanded_List_Initialisation(Machine(Space))==(skip);
Context_List_Initialisation(Machine(Space))==(skip);
List_Initialisation(Machine(Space))==(skip)
END
&
THEORY ListParametersX IS
List_Parameters(Machine(Space))==(?)
END
&
THEORY ListInstanciatedParametersX END
&
THEORY ListConstraintsX IS
List_Context_Constraints(Machine(Space))==(btrue);
List_Constraints(Machine(Space))==(btrue)
END
&
THEORY ListOperationsX IS
Internal_List_Operations(Machine(Space))==(?);
List_Operations(Machine(Space))==(?)
END
&
THEORY ListInputX END
&
THEORY ListOutputX END
&
THEORY ListHeaderX END
&
THEORY ListOperationGuardX END
&
THEORY ListPreconditionX END
&
THEORY ListSubstitutionX END
&
THEORY ListConstantsX IS
List_Valuable_Constants(Machine(Space))==(spaceX,spaceY,space,asteroids,emptySpace,homeBase,starBase);
Inherited_List_Constants(Machine(Space))==(?);
List_Constants(Machine(Space))==(spaceX,spaceY,space,asteroids,emptySpace,homeBase,starBase)
END
&
THEORY ListSetsX IS
Context_List_Enumerated(Machine(Space))==(?);
Context_List_Defered(Machine(Space))==(?);
Context_List_Sets(Machine(Space))==(?);
List_Valuable_Sets(Machine(Space))==(?);
Inherited_List_Enumerated(Machine(Space))==(?);
Inherited_List_Defered(Machine(Space))==(?);
Inherited_List_Sets(Machine(Space))==(?);
List_Enumerated(Machine(Space))==(?);
List_Defered(Machine(Space))==(?);
List_Sets(Machine(Space))==(?)
END
&
THEORY ListHiddenConstantsX IS
Abstract_List_HiddenConstants(Machine(Space))==(?);
Expanded_List_HiddenConstants(Machine(Space))==(?);
List_HiddenConstants(Machine(Space))==(?);
External_List_HiddenConstants(Machine(Space))==(?)
END
&
THEORY ListPropertiesX IS
Abstract_List_Properties(Machine(Space))==(btrue);
Context_List_Properties(Machine(Space))==(btrue);
Inherited_List_Properties(Machine(Space))==(btrue);
List_Properties(Machine(Space))==(spaceX = 1..12 & spaceY = 1..7 & space = spaceX*spaceY & asteroids <: space & asteroids = {3|->2,3|->5,5|->4,6|->7,7|->1,7|->5,7|->7,8|->3,10|->6,11|->2,12|->5} & emptySpace <: space & emptySpace/\asteroids = {} & emptySpace\/asteroids = space & homeBase: emptySpace & homeBase = 1|->1 & starBase: emptySpace & starBase = 6|->4)
END
&
THEORY ListSeenInfoX END
&
THEORY ListANYVarX END
&
THEORY ListOfIdsX IS
List_Of_Ids(Machine(Space)) == (spaceX,spaceY,space,asteroids,emptySpace,homeBase,starBase | ? | ? | ? | ? | ? | ? | ? | Space);
List_Of_HiddenCst_Ids(Machine(Space)) == (? | ?);
List_Of_VisibleCst_Ids(Machine(Space)) == (spaceX,spaceY,space,asteroids,emptySpace,homeBase,starBase);
List_Of_VisibleVar_Ids(Machine(Space)) == (? | ?);
List_Of_Ids_SeenBNU(Machine(Space)) == (?: ?)
END
&
THEORY ConstantsEnvX IS
Constants(Machine(Space)) == (Type(spaceX) == Cst(SetOf(btype(INTEGER,"[spaceX","]spaceX")));Type(spaceY) == Cst(SetOf(btype(INTEGER,"[spaceY","]spaceY")));Type(space) == Cst(SetOf(btype(INTEGER,?,?)*btype(INTEGER,?,?)));Type(asteroids) == Cst(SetOf(btype(INTEGER,?,?)*btype(INTEGER,?,?)));Type(emptySpace) == Cst(SetOf(btype(INTEGER,?,?)*btype(INTEGER,?,?)));Type(homeBase) == Cst(btype(INTEGER,?,?)*btype(INTEGER,?,?));Type(starBase) == Cst(btype(INTEGER,?,?)*btype(INTEGER,?,?)))
END
&
THEORY TCIntRdX IS
predB0 == OK;
extended_sees == KO;
B0check_tab == KO;
local_op == OK;
abstract_constants_visible_in_values == KO;
project_type == SOFTWARE_TYPE;
event_b_deadlockfreeness == KO;
variant_clause_mandatory == KO;
event_b_coverage == KO;
event_b_exclusivity == KO;
genFeasibilityPO == KO
END
)
spaceship/reasoning_cw/reasoning_cw/bdp/SpaceShip.chk
48ec6d26db03a1cc7a2f40f9a737f9fc
spaceship/reasoning_cw/reasoning_cw/bdp/SpaceShip.dep
file:229e78221a721b64e5842a767311061d
sees:Space
spaceship/reasoning_cw/reasoning_cw/bdp/SpaceShip.nf
Normalised(
THEORY MagicNumberX IS
MagicNumber(Machine(SpaceShip))==(3.5)
END
&
THEORY UpperLevelX IS
First_Level(Machine(SpaceShip))==(Machine(SpaceShip));
Level(Machine(SpaceShip))==(0)
END
&
THEORY LoadedStructureX IS
Machine(SpaceShip)
END
&
THEORY ListSeesX IS
List_Sees(Machine(SpaceShip))==(Space)
END
&
THEORY ListUsesX IS
List_Uses(Machine(SpaceShip))==(?)
END
&
THEORY ListIncludesX IS
Inherited_List_Includes(Machine(SpaceShip))==(?);
List_Includes(Machine(SpaceShip))==(?)
END
&
THEORY ListPromotesX IS
List_Promotes(Machine(SpaceShip))==(?)
END
&
THEORY ListExtendsX IS
List_Extends(Machine(SpaceShip))==(?)
END
&
THEORY ListVariablesX IS
External_Context_List_Variables(Machine(SpaceShip))==(?);
Context_List_Variables(Machine(SpaceShip))==(?);
Abstract_List_Variables(Machine(SpaceShip))==(?);
Local_List_Variables(Machine(SpaceShip))==(movements,takenRoute,noOfCollisions,power,yPosition,xPosition);
List_Variables(Machine(SpaceShip))==(movements,takenRoute,noOfCollisions,power,yPosition,xPosition);
External_List_Variables(Machine(SpaceShip))==(movements,takenRoute,noOfCollisions,power,yPosition,xPosition)
END
&
THEORY ListVisibleVariablesX IS
Inherited_List_VisibleVariables(Machine(SpaceShip))==(?);
Abstract_List_VisibleVariables(Machine(SpaceShip))==(?);
External_List_VisibleVariables(Machine(SpaceShip))==(?);
Expanded_List_VisibleVariables(Machine(SpaceShip))==(?);
List_VisibleVariables(Machine(SpaceShip))==(?);
Internal_List_VisibleVariables(Machine(SpaceShip))==(?)
END
&
THEORY ListInvariantX IS
Gluing_Seen_List_Invariant(Machine(SpaceShip))==(btrue);
Gluing_List_Invariant(Machine(SpaceShip))==(btrue);
Expanded_List_Invariant(Machine(SpaceShip))==(btrue);
Abstract_List_Invariant(Machine(SpaceShip))==(btrue);
Context_List_Invariant(Machine(SpaceShip))==(btrue);
List_Invariant(Machine(SpaceShip))==(xPosition: spaceX & yPosition: spaceY & xPosition|->yPosition: emptySpace & power: NAT & noOfCollisions: NAT & takenRoute: seq(emptySpace) & movements: seq(MOVEMENT))
END
&
THEORY ListAssertionsX IS
Expanded_List_Assertions(Machine(SpaceShip))==(btrue);
Abstract_List_Assertions(Machine(SpaceShip))==(btrue);
Context_List_Assertions(Machine(SpaceShip))==(btrue);
List_Assertions(Machine(SpaceShip))==(btrue)
END
&
THEORY ListCoverageX IS
List_Coverage(Machine(SpaceShip))==(btrue)
END
&
THEORY ListExclusivityX IS
List_Exclusivity(Machine(SpaceShip))==(btrue)
END
&
THEORY ListInitialisationX IS
Expanded_List_Initialisation(Machine(SpaceShip))==(power,noOfCollisions,xPosition,yPosition,takenRoute,movements:=initialPower,0,prj1(spaceX,spaceY)(homeBase),prj2(spaceX,spaceY)(homeBase),[homeBase],<>);
Context_List_Initialisation(Machine(SpaceShip))==(skip);
List_Initialisation(Machine(SpaceShip))==(power:=initialPower || noOfCollisions:=0 || xPosition:=prj1(spaceX,spaceY)(homeBase) || yPosition:=prj2(spaceX,spaceY)(homeBase) || takenRoute:=[homeBase] || movements:=<>)
END
&
THEORY ListParametersX IS
List_Parameters(Machine(SpaceShip))==(?)
END
&
THEORY ListInstanciatedParametersX IS
List_Instanciated_Parameters(Machine(SpaceShip),Machine(Space))==(?)
END
&
THEORY ListConstraintsX IS
List_Context_Constraints(Machine(SpaceShip))==(btrue);
List_Constraints(Machine(SpaceShip))==(btrue)
END
&
THEORY ListOperationsX IS
Internal_List_Operations(Machine(SpaceShip))==(MoveUp,MoveDown,MoveForward,MoveBackward,EngageWarpDrive,MissionStatus,MissionRoute,DockedAtStarbase,GameStatus,takenMovements,resetGame);
List_Operations(Machine(SpaceShip))==(MoveUp,MoveDown,MoveForward,MoveBackward,EngageWarpDrive,MissionStatus,MissionRoute,DockedAtStarbase,GameStatus,takenMovements,resetGame)
END
&
THEORY ListInputX IS
List_Input(Machine(SpaceShip),MoveUp)==(?);
List_Input(Machine(SpaceShip),MoveDown)==(?);
List_Input(Machine(SpaceShip),MoveForward)==(?);
List_Input(Machine(SpaceShip),MoveBackward)==(?);
List_Input(Machine(SpaceShip),EngageWarpDrive)==(newXPosition,newYPosition);
List_Input(Machine(SpaceShip),MissionStatus)==(?);
List_Input(Machine(SpaceShip),MissionRoute)==(?);
List_Input(Machine(SpaceShip),DockedAtStarbase)==(?);
List_Input(Machine(SpaceShip),GameStatus)==(?);
List_Input(Machine(SpaceShip),takenMovements)==(?);
List_Input(Machine(SpaceShip),resetGame)==(?)
END
&
THEORY ListOutputX IS
List_Output(Machine(SpaceShip),MoveUp)==(report,movement);
List_Output(Machine(SpaceShip),MoveDown)==(report,movement);
List_Output(Machine(SpaceShip),MoveForward)==(report,movement);
List_Output(Machine(SpaceShip),MoveBackward)==(report,movement);
List_Output(Machine(SpaceShip),EngageWarpDrive)==(report,movement);
List_Output(Machine(SpaceShip),MissionStatus)==(currentLocation,currentPower,asteroidCollisions);
List_Output(Machine(SpaceShip),MissionRoute)==(route);
List_Output(Machine(SpaceShip),DockedAtStarbase)==(dockedStatus);
List_Output(Machine(SpaceShip),GameStatus)==(status);
List_Output(Machine(SpaceShip),takenMovements)==(allMovements);
List_Output(Machine(SpaceShip),resetGame)==(?)
END
&
THEORY ListHeaderX IS
List_Header(Machine(SpaceShip),MoveUp)==(report,movement <-- MoveUp);
List_Header(Machine(SpaceShip),MoveDown)==(report,movement <-- MoveDown);
List_Header(Machine(SpaceShip),MoveForward)==(report,movement <-- MoveForward);
List_Header(Machine(SpaceShip),MoveBackward)==(report,movement <-- MoveBackward);
List_Header(Machine(SpaceShip),EngageWarpDrive)==(report,movement <-- EngageWarpDrive(newXPosition,newYPosition));
List_Header(Machine(SpaceShip),MissionStatus)==(currentLocation,currentPower,asteroidCollisions <-- MissionStatus);
List_Header(Machine(SpaceShip),MissionRoute)==(route <-- MissionRoute);
List_Header(Machine(SpaceShip),DockedAtStarbase)==(dockedStatus <-- DockedAtStarbase);
List_Header(Machine(SpaceShip),GameStatus)==(status <-- GameStatus);
List_Header(Machine(SpaceShip),takenMovements)==(allMovements <-- takenMovements);
List_Header(Machine(SpaceShip),resetGame)==(resetGame)
END
&
THEORY ListOperationGuardX END
&
THEORY ListPreconditionX IS
List_Precondition(Machine(SpaceShip),MoveUp)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power List_Precondition(Machine(SpaceShip),MoveDown)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power List_Precondition(Machine(SpaceShip),MoveForward)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power List_Precondition(Machine(SpaceShip),MoveBackward)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power List_Precondition(Machine(SpaceShip),EngageWarpDrive)==(report: REPORT & movement: MOVEMENT & newXPosition: NAT1 & newYPosition: NAT1 & not(xPosition|->yPosition = starBase or power List_Precondition(Machine(SpaceShip),MissionStatus)==(btrue);
List_Precondition(Machine(SpaceShip),MissionRoute)==(btrue);
List_Precondition(Machine(SpaceShip),DockedAtStarbase)==(dockedStatus: DOCKED_STATUS);
List_Precondition(Machine(SpaceShip),GameStatus)==(status: GAME_STATUS);
List_Precondition(Machine(SpaceShip),takenMovements)==(btrue);
List_Precondition(Machine(SpaceShip),resetGame)==(xPosition|->yPosition = starBase or powerEND
&
THEORY ListSubstitutionX IS
Expanded_List_Substitution(Machine(SpaceShip),resetGame)==(xPosition|->yPosition = starBase or power);
Expanded_List_Substitution(Machine(SpaceShip),takenMovements)==(btrue | allMovements:=movements);
Expanded_List_Substitution(Machine(SpaceShip),GameStatus)==(status: GAME_STATUS | xPosition|->yPosition = starBase ==> status:=GAME_WON [] not(xPosition|->yPosition = starBase) ==> (power status:=GAME_LOST [] not(power status:=GAME_NOT_OVER));
Expanded_List_Substitution(Machine(SpaceShip),DockedAtStarbase)==(dockedStatus: DOCKED_STATUS | xPosition|->yPosition = starBase ==> dockedStatus:=YES [] not(xPosition|->yPosition = starBase) ==> dockedStatus:=NO);
Expanded_List_Substitution(Machine(SpaceShip),MissionRoute)==(btrue | route:=takenRoute);
Expanded_List_Substitution(Machine(SpaceShip),MissionStatus)==(btrue | currentLocation,currentPower,asteroidCollisions:=xPosition|->yPosition,power,noOfCollisions);
Expanded_List_Substitution(Machine(SpaceShip),EngageWarpDrive)==(report: REPORT & movement: MOVEMENT & newXPosition: NAT1 & newYPosition: NAT1 & not(xPosition|->yPosition = starBase or power=warpDrivePower ==> (newXPosition|->newYPosition: space ==> (newXPosition = xPosition & newYPosition = yPosition ==> report:=CANNOT_WARP_TO_THE_SAME_POSITION [] not(newXPosition = xPosition & newYPosition = yPosition) ==> (size(takenRoute) = 1 & newXPosition|->newYPosition = starBase ==> report:=CANNOT_IMMEDIATELY_WARP_INTO_STARBASE [] not(size(takenRoute) = 1 & newXPosition|->newYPosition = starBase) ==> (not(newXPosition|->newYPosition: asteroids) ==> (power-warpDrivePower>=0 ==> power,xPosition,yPosition,takenRoute,movements,report,movement:=power-warpDrivePower,newXPosition,newYPosition,takenRoute<-(newXPosition|->newYPosition),movements<-WARP,SUCCESSFULLY_MOVED,WARP [] not(power-warpDrivePower>=0) ==> power,xPosition,yPosition,takenRoute,movements,report,movement:=0,newXPosition,newYPosition,takenRoute<-(newXPosition|->newYPosition),movements<-WARP,SUCCESSFULLY_MOVED,WARP) [] not(not(newXPosition|->newYPosition: asteroids)) ==> report:=CANNOT_WARP_INTO_ASTEROID))) [] not(newXPosition|->newYPosition: space) ==> report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE) [] not(power>=warpDrivePower) ==> report:=INSUFFICIENT_POWER);
Expanded_List_Substitution(Machine(SpaceShip),MoveBackward)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power=normalMovePower ==> (xPosition-1|->yPosition: space ==> (not(xPosition-1|->yPosition: asteroids) ==> (power-normalMovePower>=0 ==> xPosition,power,takenRoute,movements,report,movement:=xPosition-1,power-normalMovePower,takenRoute<-(xPosition-1|->yPosition),movements<-MOVE_BACKWARD,SUCCESSFULLY_MOVED,MOVE_BACKWARD [] not(power-normalMovePower>=0) ==> xPosition,power,takenRoute,movements,report,movement:=xPosition-1,0,takenRoute<-(xPosition-1|->yPosition),movements<-MOVE_BACKWARD,SUCCESSFULLY_MOVED,MOVE_BACKWARD) [] not(not(xPosition-1|->yPosition: asteroids)) ==> (power-normalMovePower-asteroidHitPowerLoss>=0 ==> power,noOfCollisions,report,movement:=power-normalMovePower-asteroidHitPowerLoss,noOfCollisions+1,HIT_ASTEROID,MOVE_BACKWARD [] not(power-normalMovePower-asteroidHitPowerLoss>=0) ==> power,noOfCollisions,report,movement:=0,noOfCollisions+1,HIT_ASTEROID,MOVE_BACKWARD)) [] not(xPosition-1|->yPosition: space) ==> report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE) [] not(power>=normalMovePower) ==> report:=INSUFFICIENT_POWER);
Expanded_List_Substitution(Machine(SpaceShip),MoveForward)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power=normalMovePower ==> (xPosition+1|->yPosition: space ==> (not(xPosition+1|->yPosition: asteroids) ==> (power-normalMovePower>=0 ==> xPosition,power,takenRoute,movements,report,movement:=xPosition+1,power-normalMovePower,takenRoute<-(xPosition+1|->yPosition),movements<-MOVE_FORWARD,SUCCESSFULLY_MOVED,MOVE_FORWARD [] not(power-normalMovePower>=0) ==> xPosition,power,takenRoute,movements,report,movement:=xPosition+1,0,takenRoute<-(xPosition+1|->yPosition),movements<-MOVE_FORWARD,SUCCESSFULLY_MOVED,MOVE_FORWARD) [] not(not(xPosition+1|->yPosition: asteroids)) ==> (power-normalMovePower-asteroidHitPowerLoss>=0 ==> power,noOfCollisions,report,movement:=power-normalMovePower-asteroidHitPowerLoss,noOfCollisions+1,HIT_ASTEROID,MOVE_FORWARD [] not(power-normalMovePower-asteroidHitPowerLoss>=0) ==> power,noOfCollisions,report,movement:=0,noOfCollisions+1,HIT_ASTEROID,MOVE_FORWARD)) [] not(xPosition+1|->yPosition: space) ==> report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE) [] not(power>=normalMovePower) ==> report:=INSUFFICIENT_POWER);
Expanded_List_Substitution(Machine(SpaceShip),MoveDown)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power=normalMovePower ==> (xPosition|->yPosition-1: space ==> (not(xPosition|->yPosition-1: asteroids) ==> (power-normalMovePower>=0 ==> yPosition,power,takenRoute,movements,report,movement:=yPosition-1,power-normalMovePower,takenRoute<-(xPosition|->yPosition-1),movements<-MOVE_DOWN,SUCCESSFULLY_MOVED,MOVE_DOWN [] not(power-normalMovePower>=0) ==> yPosition,power,takenRoute,movements,report,movement:=yPosition-1,0,takenRoute<-(xPosition|->yPosition-1),movements<-MOVE_DOWN,SUCCESSFULLY_MOVED,MOVE_DOWN) [] not(not(xPosition|->yPosition-1: asteroids)) ==> (power-normalMovePower-asteroidHitPowerLoss>=0 ==> power,noOfCollisions,report,movement:=power-normalMovePower-asteroidHitPowerLoss,noOfCollisions+1,HIT_ASTEROID,MOVE_DOWN [] not(power-normalMovePower-asteroidHitPowerLoss>=0) ==> power,noOfCollisions,report,movement:=0,noOfCollisions+1,HIT_ASTEROID,MOVE_DOWN)) [] not(xPosition|->yPosition-1: space) ==> report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE) [] not(power>=normalMovePower) ==> report:=INSUFFICIENT_POWER);
Expanded_List_Substitution(Machine(SpaceShip),MoveUp)==(report: REPORT & movement: MOVEMENT & not(xPosition|->yPosition = starBase or power=normalMovePower ==> (xPosition|->yPosition+1: space ==> (not(xPosition|->yPosition+1: asteroids) ==> (power-normalMovePower>=0 ==> yPosition,power,takenRoute,movements,report,movement:=yPosition+1,power-normalMovePower,takenRoute<-(xPosition|->yPosition+1),movements<-MOVE_UP,SUCCESSFULLY_MOVED,MOVE_UP [] not(power-normalMovePower>=0) ==> yPosition,power,takenRoute,movements,report,movement:=yPosition+1,0,takenRoute<-(xPosition|->yPosition+1),movements<-MOVE_UP,SUCCESSFULLY_MOVED,MOVE_UP) [] not(not(xPosition|->yPosition+1: asteroids)) ==> (power-normalMovePower-asteroidHitPowerLoss>=0 ==> power,noOfCollisions,report,movement:=power-normalMovePower-asteroidHitPowerLoss,noOfCollisions+1,HIT_ASTEROID,MOVE_UP [] not(power-normalMovePower-asteroidHitPowerLoss>=0) ==> power,noOfCollisions,report,movement:=0,noOfCollisions+1,HIT_ASTEROID,MOVE_UP)) [] not(xPosition|->yPosition+1: space) ==> report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE) [] not(power>=normalMovePower) ==> report:=INSUFFICIENT_POWER);
List_Substitution(Machine(SpaceShip),MoveUp)==(IF power>=normalMovePower THEN IF xPosition|->yPosition+1: space THEN IF not(xPosition|->yPosition+1: asteroids) THEN IF power-normalMovePower>=0 THEN yPosition:=yPosition+1 || power:=power-normalMovePower || takenRoute:=takenRoute<-(xPosition|->yPosition+1) || movements:=movements<-MOVE_UP || report:=SUCCESSFULLY_MOVED || movement:=MOVE_UP ELSE yPosition:=yPosition+1 || power:=0 || takenRoute:=takenRoute<-(xPosition|->yPosition+1) || movements:=movements<-MOVE_UP || report:=SUCCESSFULLY_MOVED || movement:=MOVE_UP END ELSE IF power-normalMovePower-asteroidHitPowerLoss>=0 THEN power:=power-normalMovePower-asteroidHitPowerLoss || noOfCollisions:=noOfCollisions+1 || report:=HIT_ASTEROID || movement:=MOVE_UP ELSE power:=0 || noOfCollisions:=noOfCollisions+1 || report:=HIT_ASTEROID || movement:=MOVE_UP END END ELSE report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE END ELSE report:=INSUFFICIENT_POWER END);
List_Substitution(Machine(SpaceShip),MoveDown)==(IF power>=normalMovePower THEN IF xPosition|->yPosition-1: space THEN IF not(xPosition|->yPosition-1: asteroids) THEN IF power-normalMovePower>=0 THEN yPosition:=yPosition-1 || power:=power-normalMovePower || takenRoute:=takenRoute<-(xPosition|->yPosition-1) || movements:=movements<-MOVE_DOWN || report:=SUCCESSFULLY_MOVED || movement:=MOVE_DOWN ELSE yPosition:=yPosition-1 || power:=0 || takenRoute:=takenRoute<-(xPosition|->yPosition-1) || movements:=movements<-MOVE_DOWN || report:=SUCCESSFULLY_MOVED || movement:=MOVE_DOWN END ELSE IF power-normalMovePower-asteroidHitPowerLoss>=0 THEN power:=power-normalMovePower-asteroidHitPowerLoss || noOfCollisions:=noOfCollisions+1 || report:=HIT_ASTEROID || movement:=MOVE_DOWN ELSE power:=0 || noOfCollisions:=noOfCollisions+1 || report:=HIT_ASTEROID || movement:=MOVE_DOWN END END ELSE report:=CANNOT_MOVE_OUT_OF_KNOWN_SPACE END ELSE report:=INSUFFICIENT_POWER...
SOLUTION.PDF

Answer To This Question Is Available To Download

Related Questions & Answers

More Questions »

Submit New Assignment

Copy and Paste Your Assignment Here