README

This is a project completed in the Forge constraint language to model valid games (at a smaller scale) of the boardgame Battleship.

1. We are trying to model a valid game of Battleship from start to finish. This boardgame involves two players with ships they place on a grid that is unknown to their opponent. Players then take turns picking a coordinate on their opponent's board to attack (which they have not attacked before), and the opponent must state whether this was a hit (on one of their ships) or a miss (on open water). We want to model a valid sequence of such guesses that, assuming the ship placement is given, random, and wellformed at the start of our model, results in one of the players winning by sinking all of their opponent's ships with some of their own still unsink. A ship is sunk when all the coordinates it occupies have been attacked.

2. One thing we chose not to model was the process of player's ship placement; we just assume that at the start of our trace that the ships have been placed validly by each player (and enforce this validity of placement on our init State). This is because the process of ship placement does not have any specific rules besides the fact that it must be done and done validly by both players before turns of attacking begin. In the real boardgame, player's have a secondary grid that they place red and white pegs on to track where on their opponent's grid they've attacked and the result of these moves (red for a hit, white for a miss). We also did not model this because it is a tool to help human players play the game well, but is not technically part of the game (in the sense that a player tracking this can do things that aren't wellformed and the game can still proceed and be played in a valid way) nor necessary to play. The other significant decision we made regarding how to model the game was sizing it down to run in Forge in a reasonable amount of time, and so that we could make reasonable sense of the Table as we developed the model. The real game uses a 10x10 board and 5 ships per player. We worked on a 3x3 board and gave each player 1 ship. This had the effect of keeping the amount of Int's we needed lower, the amount of Coordinates we needed lower (in an exponential way), and the amount of States in a complete trace way lower. However, it still allowed us to do property based testing on what was a scaled-back, but still essentially the same, version of the game. We modeled the two 3x3 grids (one for each player's ship) as a single 3x6 grid, and added predicates to keep each player's ships on their half of this combined board. The checks we have make sure that our model behaves correctly throughout traces, after the game has ended, and ensures some properties that are derived (rather than specifically mentioned in a predicate) hold true. The run statements we have is the most optimized/constrained universe that allows every possible game in our model. 19 States are needed for their to be an init State along with hitting all 18 coordinates on our 3x6 grid, their our exactly 2 ships in our model (one destroyer for each player/fleet), and we need exactly 18 coordinates (which we constrain to be unique and the right ones in our model). In retrospect we could have further optimized by running on 3 Int and utilizing negative numbers to have our board y-coordinates go from -3 to 2 instead of 0 to 5, but such is the wisdom of hindsight. We find it easiest to interpret Sterling by going to the Table where it is easiest to see what ships belong to what player/fleet, what their coordinates are, and what attacks are taken. Attacks are entries under the board relation. The Graph, even when projecting over State, is very hard to decipher due to the amount of things in our instances.

3. The sigs we have make a Game with States that start with an initial state and are linked through a next relation (that is made linear at run). We have an abstract Ship sig that our types of ship (in our model only a destroyer) extend. The singleton Yes sig allows us to see what coordinates on the board a ship is on; the Coordinate sig, speaking of which, are exactly one in number for the 18 spots on our 3x6 grid (thanks to inBoundsCoordinates and noDuplicateCoordinates predicates). The Fleet sig represents our players (each player, A and B, has one Fleet, so we modeled them one in the same) and each State sig has a board relation that relates a Coordinate (with it's unique x and y positining) to a Fleet; this relation is a pfunc so that it can be none for a given coordinate, indicating that coordinate has not been attacked yet in that state. The differentShipsInEachFleet solves a bug we were having where different Fleets were using the same ship. The lengths predicate makes sure all Ships have their length, which is how many coordinates they occupy, is set to their actual value from the real version of the boardgame. The init predicate makes sure the initial state has no attacks that have been done, ATurn and BTurn are used in conjunction with validTransition to make sure that attacks alternate between players and that transitions between states are good. The predicates wellformed, gameOver, doNothing, and traces all make sure the game is a trace of States that follow the rules of the game.

4. What we learned doing this is how long Forge can take to run on large universes, and thus many tricks for optimization. It also helped us to think more clearly about what was important in our domain, and thus what we could eliminate as being of essentially the same nature (e.g., a bigger board), what we could model cleverly so as to reduce the difficulty of writing constraints (e.g., the combined single 3x6 board), all without losing the spirit (really the important properties) of what we were trying to model.