Answer To: Coursework Description 1. Introduction This coursework requires you to develop a B specification of...
Amar Kumar answered on Oct 29 2021
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 |-> yPosition : 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...