debug this code

and check whether the following works successfully or not?

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

MACHINE Battleship

SETS

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

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

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

Reports $=\{$Hit$,$ Miss, InvalidMove$\}$;

CONSTANTS

Grid, FleetSize

PROPERTIES

Grid $=(1\mathrm{.}10)*(1\mathrm{.}10)$ & $/*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 and

player$2$Ships $<$: Grid &

card$($player$1$Ships$)<=$ FleetSize &

card$($player$2$Ships$)<=$ FleetSize &

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

player$1$Shots $<$: Grid &

player$2$Shots $<$: Grid &

currentPlayer : Players &

gameState : GameStates

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 \backslash$ player$2$Ships $=\{\})$ &

$($player $=$ Player$2=>$ positions $/\backslash \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: shipLocations $*/$

shipsquares $<--$ shipLocations$($player$)=$

PRE

player : Players

THEN

IF player $=$ Player$1$ THEN

shipsquares :$=$ player$1$Ships

ELSE

shipsquares :$=$ player$2$Ships

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