use ATELIER B$...$GIVE THE WHOLE CODE WITHOUT MISTAKES $($attached here is a code for ur reference use it when forming the GRID and where necessary the coding practice shud follow the given example the $....$project shud run in atelier B and pro b and give the working code

ps$.$ plz check the SETS specially$)$

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.

example code.....

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