this is the code i came up with edit this according to the example code given below.

MACHINE

Battleships

SETS

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

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

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 : Status

INITIALISATION

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

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

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

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

currentPlayer :$=$ Player$1||$

gameState :$=$ Deploying

OPERATIONS

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"

ELSE

report :$=$ "Invalid positions"

END;

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

ELSE

report :$=$ "Invalid move"

END;

shipsquares shipLocations$($player$)=$

PRE

player : Players

THEN

IF player $=$ Player$1$ THEN

shipsquares :$=$ player$1$Ships

ELSE

shipsquares :$=$ player$2$Ships

END

END;

shipCounts shipsLeft $=$

BEGIN

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

END;

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;

report gameStatus $=$

BEGIN

report :$=$ gameState

END;

END

$----$example code for GRID and the code writing$----$

MACHINE

NoughtsCrosses

SETS

Players $=\{$Noughts$,$ Crosses$\}$;

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

CONSTANTS

Grid, winningSubsets

PROPERTIES

Grid $=(1.\mathrm{.}3)*(1.\mathrm{.}3)$ &

winningSubsets $$: POW$($Grid$)$ &

winningSubsets $=\{\{1\}*(1.\mathrm{.}3),\{2\}*(1.\mathrm{.}3),\{3\}*(1.\mathrm{.}3),$

$(1.\mathrm{.}3)*\{1\},(1.\mathrm{.}3)*\{2\},(1.\mathrm{.}3)*\{3\},$

id$(1.\mathrm{.}3),\{1|->3,2|->2,3|->1\}\}$

VARIABLES

noughts, crosses

INVARIANT

noughts $$: Grid & crosses $$: Grid & noughts $/\backslash$ crosses $=\{\}$

INITIALISATION

noughts :$=\{\}||$ crosses :$=\{\}$

OPERATIONS

res placeNought$($pp$)=$

PRE

pp : Grid

THEN

IF

pp : noughts $\backslash /$ crosses

THEN

res :$=$ Failure

ELSE

noughts :$=$ noughts $\backslash /\{$ pp $\}||$

res :$=$ Success

END

END;

res placeCross$($pp$)=$

PRE

pp : Grid

THEN

IF

pp : noughts $\backslash /$ crosses

THEN

res :$=$ Failure

ELSE

crosses :$=$ crosses $\backslash /\{$ pp $\}||$

res :$=$ Success

END

END

END