the code i came up with for the battleship exercise is attached here.

MACHINE BATTLE

SETS

Players $=\{$Player$1,$ Player$2\}$;

Results $=\{$Success$,$ Failure$\}$;

GameStates $=\{$Deploying$,$ Ongoing, Player$1$Win, Player$2$Win$\}$;

Reports $=\{$Hit$,$ Miss, InvalidMove$\}/*$ Declare gameState values explicitly $*/$

CONSTANTS

Grid, FleetSize

PROPERTIES

Grid $=(1.\mathrm{.}10)*(1.\mathrm{.}10)$ & $/*$ A $10$x$10$ grid $*/$

FleetSize $=3/*$ Each player has $3$ ships $*/$

VARIABLES

player$1$Ships, player$2$Ships, $/*$ Positions of Player $1\text{'}$s and Player $2\text{'}$s ships $*/$

player$1$Shots, player$2$Shots, $/*$ Shots taken by Player $1$ and Player $2*/$

currentPlayer, $/*$ Whose turn it is $*/$

gameState $/*$ Current state of the game $*/$

INVARIANT

player$1$Ships $$: Grid &

player$2$Ships $$: Grid &

card$($player$1$Ships FleetSize &

card$($player$2$Ships FleetSize &

player$1$Ships $/\backslash$ player$2$Ships $=\{\}$ & $/*$ No overlapping ships $*/$

player$1$Shots $$: Grid &

player$2$Shots $$: Grid &

currentPlayer : Players &

gameState : GameStates $/*$ Use the explicitly declared GameStates set $*/$

INITIALISATION

player$1$Ships :$=\{\}||$

player$2$Ships :$=\{\}||$

player$1$Shots :$=\{\}||$

player$2$Shots :$=\{\}||$

currentPlayer :$=$ Player$1||$

gameState :$=$ Deploying

OPERATIONS

$/*$ Deploy Fleet Operation $*/$

report deployFleet$($player$,$ positions$)=$

PRE

player : Players &

positions $$: Grid &

card$($positions$)=$ FleetSize &

$(($player $=$ Player$1=>$ player$1$Ships $=\{\})$ &

$($player $=$ Player$2=>$ player$2$Ships $=\{\}))$ &

$(($player $=$ Player$1=>$ positions $/\backslash$ player$2$Ships $=\{\})$ &

$($player $=$ Player$2=>$ positions $/\backslash$ player$1$Ships $=\{\}))$

THEN

IF player $=$ Player$1$ THEN

player$1$Ships :$=$ positions

ELSE

player$2$Ships :$=$ positions

END $||$

IF player$1$Ships $/=\{\}$ & player$2$Ships $/=\{\}$ THEN

gameState :$=$ Ongoing

END $||$

report :$=$ Success

END;

$/*$ Player Shoots Operation $*/$

report playerShoots$($target$)=$

PRE

target : Grid &

gameState $=$ Ongoing

THEN

IF currentPlayer $=$ Player$1$ THEN

IF target : player$2$Ships THEN

player$2$Ships :$=$ player$2$Ships $-\{$target$\}||$

report :$=$ Hit $||$

IF card$($player$2$Ships$)=0$ THEN

gameState :$=$ Player$1$Win

ELSE

currentPlayer :$=$ Player$2$

END

ELSE

report :$=$ Miss $||$

currentPlayer :$=$ Player$2$

END $||$

player$1$Shots :$=$ player$1$Shots $\backslash /\{$target$\}$

ELSE

IF target : player$1$Ships THEN

player$1$Ships :$=$ player$1$Ships $-\{$target$\}||$

report :$=$ Hit $||$

IF card$($player$1$Ships$)=0$ THEN

gameState :$=$ Player$2$Win

ELSE

currentPlayer :$=$ Player$1$

END

ELSE

report :$=$ Miss $||$

currentPlayer :$=$ Player$1$

END $||$

player$2$Shots :$=$ player$2$Shots $\backslash /\{$target$\}$

END

END;

$/*$ Enquiry Operation: shipsLeft $*/$

shipCounts shipsLeft $=$

BEGIN

shipCounts :$=\{$Player$1|->$ card$($player$1$Ships$),$ Player$2|->$ card$($player$2$Ships$)\}$

END;

$/*$ Enquiry Operation: shotsTaken $*/$

shotCount shotsTaken$($player$)=$

PRE

player : Players

THEN

IF player $=$ Player$1$ THEN

shotCount :$=$ card$($player$1$Shots$)$

ELSE

shotCount :$=$ card$($player$2$Shots$)$

END

END;

$/*$ Enquiry Operation: gameStatus $*/$

report gameStatus $=$

BEGIN

report :$=$ gameState

END

END

can u check whether the code is correct when animated in PRO B$?$

The Battleships game is played as follows:

$1.$ The game starts by each player placing their $3$ ships on their own grid, each player's ships in different grid squares.

$2.$ Player $1$ has the first turn.

$3.$ Player $1$ shoots at Player $2\text{'}$s ships, by selecting a target square on Player $2\text{'}$s grid. If there is a ship in the target square it is a hit and the ship is deleted from Player $2\text{'}$s fleet, otherwise it is a miss and there is no change to Player $2\text{'}$s fleet.

$4.$ It is then Player $2\text{'}$s turn.

$5.$ Player $2$ shoots at Player $1\text{'}$s ships, by selecting a target square on Player $1\text{'}$s grid. Registering a hit or miss, as above.

$6.$ The players continue to take turns until all of one player's ships have been sunk, at this point the other player is the winner.

could u check whether the following works successfully or not?

deployFleet operation, playerShoots operation, shipLocations operation, shipsLeft operation, shotsTaken operation, gameStatus operation

else plz attach the edited code where these will work successfully.