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

$2\mathrm{.}1$ Specification Components

Your B specification should include the following elements.

$($a$)$ Sets and Constants

Any sets and constants that are required to define the data and state of the Battleships game system, and their properties.

Includes at least the set of players, dimensions of their grids, and number of battleships.

$($b$)$ System State

The state variables required to represent the data for the Battleships game system. Including the state invariant and initialisation.

Includes at least both players$$ grids, the current game state $($for example, it could be ongoing, won by either player, or one or both players may still need to deploy their fleet$),$ and whose turn it is$.$ Check the operations to figure out what other information is needed.

$($c$)$ Operations

The Battleships game operations are:

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

The specified player places their $3$ ships at the given positions on their own grid. If the ships are all placed in valid grid positions, then the operation reports success, otherwise it reports an error message indicating what the error was.

report playerShoots$($target$)$

The player whose turn it is shoots at the target square on the other player's grid. If it contains a ship, then this ship is deleted, and the operation reports a hit. If this was their last ship the game is over, and the current player wins the game; otherwise, it is the other player$$s turn. If there is no ship in the target square the operation reports a miss. If the target square is not in the grid, it reports an error message.

For each operation make sure to use suitable preconditions $($e$.$g$.$ players should not start shooting before both fleets have been deployed$).$

$($d$)$ Enquiry Operations

You must also specify the following enquiry operations, that all output information about the state of the game:

shipsquares shipLocations$($player$)$

Outputs the location of all the ships left in the player's fleet.

shipCounts shipsLeft

Outputs the numbers of ships left in both players$$ fleets.

shotCount shotsTaken$($player$)$

Outputs the number of shots taken by the player.

report gameStatus

Gives information about the game$$s state $($e$.$g$.$ ongoing, player $1$ win, both players still need to deploy, etc$)$

$2\mathrm{.}2$ General Requirements

The B specification should use the appropriate features to define the data & operations in any machines that you define. The overall structure of the B specification can be either:

$$ A single B machine that contains all the state information and operations, etc.

$$ A collection of B machines that together contain all the state information and operations, etc. The appropriate B structuring features must be used to combine the collection of B machines.