use ATELIER B$...$GIVE THE WHOLE CODE WITHOUT MISTAKES PLZZZ $($attached here is a code for ur ease but there are some errors here, adjust the code and run it in atelier B and pro b and give the working code ps$.)$

code shud compulsorily have these code lines,

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

report playerShoots$($target$)$

shipsquares shipLocations$($player$)$

shipCounts shipsLeft

shotCount shotsTaken$($player$)$

report gameStatus

This system is to be developed using the B tools Atelier B and ProB.

$$ A grid size of $10$ x $10$ squares, with the grid square $(6,8)$ representing the square at column $6$ & row $8.$

$$ Each player has $3$ warships in their fleet.

$$ Each warship occupies a single grid square on the grid.

$$ The warships must be on different grid squares, i$.$e$.$ at most $1$ warship per square.

$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.

MACHINE battlecw

SETS

ROWS; COLS; PLAYER

CONSTANTS

ROWS$\_$SET, COLS$\_$SET, PLAYER$\_$SET, SHIPS$\_$COUNT

PROPERTIES

ROWS$\_$SET $=\{1,2,3,4,5,6,7,8,9,10\}$ &

COLS$\_$SET $=\{1,2,3,4,5,6,7,8,9,10\}$ &

PLAYER$\_$SET $=\{1,2\}$ &

SHIPS$\_$COUNT $=3$

VARIABLES

grid$1,$ grid$2,//$ Grid for player $1$ and player $2$

ships$\_$left$1,$ ships$\_$left$2,//$ Ships left for player $1$ and player $2$

current$\_$player, $//$ The current player

game$\_$status $//$ Game status $($TRUE for ongoing, FALSE for ended$)$

INVARIANT

grid$1$ : ROWS $*$ COLS $-->$ BOOL & $//$ Grid $1$ contains boolean values

grid$2$ : ROWS $*$ COLS $-->$ BOOL & $//$ Grid $2$ contains boolean values

ships$\_$left$1$ : NAT & ships$\_$left SHIPS$\_$COUNT &

ships$\_$left$2$ : NAT & ships$\_$left SHIPS$\_$COUNT &

current$\_$player : PLAYER &

game$\_$status : BOOL

INITIALISATION

grid$1$ :$=($ROWS $*$ COLS FALSE $||//$ Initially no ships on grid $1$

grid$2$ :$=($ROWS $*$ COLS FALSE $||//$ Initially no ships on grid $2$

ships$\_$left$1$ :$=$ SHIPS$\_$COUNT $||$

ships$\_$left$2$ :$=$ SHIPS$\_$COUNT $||$

current$\_$player :$=1||$

game$\_$status :$=$ TRUE

OPERATIONS

$//$ Deploy fleet operation

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

PRE

player : PLAYER &

positions $$: ROWS $*$ COLS &

card$($positions$)=$ SHIPS$\_$COUNT &

$!$pos. $($pos : positions $=>($player $=1=>$ grid$1($pos$)=$ FALSE$)$ & $($player $=2=>$ grid$2($pos$)=$ FALSE$))$

THEN

IF player $=1$ THEN

grid$1$ :$=$ grid positions TRUE

ELSE

grid$2$ :$=$ grid positions TRUE

END;

report :$=$ "Success"

ELSE

report :$=$ "Error: Invalid positions"

END;

$//$ Player shoots operation

report playerShoots$($target$)=$

PRE

target : ROWS $*$ COLS &

game$\_$status $=$ TRUE

THEN

IF current$\_$player $=1$ THEN

IF grid$2($target$)=$ TRUE THEN

grid$2($target$)$ :$=$ FALSE;

ships$\_$left$2$ :$=$ ships$\_$left$2-1$;

IF ships$\_$left$2=0$ THEN

game$\_$status :$=$ FALSE;

report :$=$ "Player $1$ Wins!"

ELSE

report :$=$ "Hit!"

END

ELSE

report :$=$ "Miss!"

END;

current$\_$player :$=2$

ELSE

IF grid$1($target$)=$ TRUE THEN

grid$1($target$)$ :$=$ FALSE;

ships$\_$left$1$ :$=$ ships$\_$left$1-1$;

IF ships$\_$left$1=0$ THEN

game$\_$status :$=$ FALSE;

report :$=$ "Player $2$ Wins!"

ELSE

report :$=$ "Hit!"

END

ELSE

report :$=$ "Miss!"

END;

current$\_$player :$=1$

END

ELSE

report :$=$ "Error: Invalid target"

END;

$//$ Get ship locations

shipsquares shipLocations$($player$)=$

PRE

player : PLAYER

THEN

IF player $=1$ THEN

shipsquares :$=\{$pos $|$ pos : ROWS $*$ COLS & grid$1($pos$)=$ TRUE$\}$

ELSE

shipsquares :$=\{$pos $|$ pos : ROWS $*$ COLS & grid$2($pos$)=$ TRUE$\}$

END

END;

$//$ Get ships left

shipCounts shipsLeft $=$

BEGIN

shipCounts :$=($ships$\_$left$1,$ ships$\_$left$2)$

END;

$//$ Get game status

report gameStatus $=$

BEGIN

IF game$\_$status THEN

report :$=$ "Ongoing"

ELSE

IF ships$\_$left$1=0$ THEN

report :$=$ "Player $2$ Wins!"

ELSE

report :$=$ "Player $1$ Wins!"

END

END

END;

END

battlecw.mch

player : PLAYER &

positions $$: ROWS $*$ COLS &

card$($positions$)=$ SHIPS$\_$COUNT &

$!$pos. $($pos : positions $=>($player $=1=>$ grid$1($pos$)=$ FALSE$)$ & $($player $=2=>$ grid$2($pos$)=$

FALSE$))$

THEN

IF player $=1$ THEN

gridl :$=$ gridl positions TRUE

ELSE

grid$2$ :$=$ grid positions TRUE

END;

report :$=$ "Success"

ELSE

report :$=$ "Error: Invalid positions"

END;

$//$ Player shoots operation

report playerShoots$($target$)=$

PRE

target : ROWS $*$ COLS &

game$\_$status $=$ TRUE

THEN

IF current$\_$player $=1$ THEN

IF grid$2($target$)=$ TRUE THEN

grid$2($target$)$ :$=$ FALSE;

shins left$\mathrm{.}2$ :$=$ shins left$\mathrm{.}2-1$:

batleow.mch

player : PLAYER &

positions $$: ROWS $*$ COLS &

card$($positions$)=$ SHIPS$\_$COUNT &

$!$pos. $($pos : positions $=>($player $=1=>$ grid$1($pos$)=$ FALSE$)$ & $($player $=2=>$ grid$2($pos$)=$

FALSE$))$

THEN

IF player $=1$ THEN

gridl :$=$ gridl positions $$

ELSE

grid$2$ :$=$ grid positions TRUE

END;

report :$=$ "Success"

ELSE

report :$=$ "Error: Invalid positions"

END;