this is the code i came up with for the coursework battleship its attached here. edit this according to the example code given below the example code is attached to follow the coding practice

the error i get is also attached here as a snippet

MACHINE battlecw

SETS

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

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

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 : $\{$Deploying$,$ Ongoing, Player$1$Win, Player$2$Win$\}$

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

ELSE

report :$=$ Failure

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

ELSE

report :$=$ "Invalid move"

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

$----$example code for 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