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

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