Connect4 Forge Model as part of CS171 Final Project
When we set off to model Connect 4, we had hoped to model a game we were not only familiar with but also interested in. Our base goal was to implement a functioning model that accurately depicts how a game of Connect 4 is played, sticking true to its rules and policies. Our second goal was to compare and observe different strategies employed when playing the game. We knew that Connect 4 is a solved game, and were intrigued by the different combinations of strategies and how they can affect the outcome of the game.
For the base of the game, we began with implementing a model in full forge. After finishing the initial implementation, we realized that temporal forge would be more beneficial to our goals of implementing strategies. The rationale behind experimenting with temporal forge was to maintain a foundation that is most friendly to employing game strategies. Using temporal functionality, in theory, would have made it more user-friendly to implement and write different game strategies as we transition from one state to the other, and detect when a game reaches a winning or draw state. Thus, we would be unable to visually trace how the board is moving and whether the strategies we coded were being employed correctly and successfully. We pivoted to reimplementing our model in temporal forge, but were ultimately unsuccessful in getting the model to work. The temporal forge model was able to provide winning instances for Connect 4, but the traces did not properly show each move or follow the turn-based play of the game. Due to time constraints, we switched back to our old model and figured out ways to modify our traces predicate in order to implement strategies for the different players of the game. The non-temporal implementation allowed us to view different boards using our visualizer and track the different moves each of the players was making.
For how we modeled the game, we created a Player sig that represents the X and O players. We create a Board sig to keep track of the state of the board. The board field of the Board sig, when given a row and column, shows which player is placed on that exact location on the board. We create a Game sig that holds the "initialState" and has a field "next" that serves as our transition signifier from a previous board to the next one. We model a 6 x 7 board and confirm these parameters by checking our board using a wellformed predicate. This predicate confines the maximum number of rows and columns and makes sure no player is making moves outside of the 6 x 7 params. Our starting and initial state, we define using a predicate called 'starting'. This predicate ensures that the board starts out empty, with neither player having made any moves. Our move predicate represents the transition from a previous to a next state. Given a previous board, next board, a row, a column, and a player, it checks that it's the player's turn and the place they would like to move is unoccupied. The move predicate also ensures that the player is only moving to a place where there is a piece below it or it is moving to the first row in order to keep consistent with the rules of connect four. The move predicate also ensures that the only difference between the previous board and the next board is the changed piece indicated by the given row, column, and player. In order to check that players are alternating, we write two predicates called Xturn and Oturn. Xturn, defines X as our first player, and ensures X only places when there is an even number of pieces on the board. Oturn, on the other hand, infers its turn when there is an odd number of pieces on the board.
Our traces start the game by defining a Game’s initial state. Then, we look at all boards and make sure that each of them is either reached by using the move predicate or by doing nothing (when a player has won a game). We check if there is a winner on the board by calling our win predicate that checks for a sequence of 4 same player pieces on a board. If there is no winner on the board, we call our move function. We employ our different strategies when deciding where the next player will be placing their piece, i.e choosing what the next row and column are depending on whether the player is X or O.
Our biggest challenge with the model was the traces predicate. We spent a lot of time trying to figure out how to get the game to stop move transitions once a player had won the game. The main reason this predicate was not working for us was the structure we were using, where our if else statement was not truly constraining movement if a player had won. Once we figured this issue out, with the help of Professor Nelson and the TAs, we were able to make much more progress with developing strategies.
Another small challenge we ran into was the visualizer. Our visualizer was not properly fitting within the bounds of the screen, so we were not able to view all the boards. This was fixed by simply changing the x and y offset of the boards. We also were not able to get the visualizer working for the temporal mode of our model because it was not able to properly visualize the transitions between boards.
The final challenges we had were focused on the strategy comparison and the board limits. We were not able to implement extremely complex strategies due to not getting temporal mode working. Because we could not implement complex strategies, we did not have any strategies that would be guaranteed to win every time. This meant that if we wanted to compare strategies, it was impossible to come up with a definitive outcome for which strategy is better. We resorted to comparing strategies to each other visually and running traces of various players employing various strategies to see how they compared.
When we set off to complete the project, we went in knowing that Connect 4 is a solved game. We had hoped to be able to employ that winning strategy, however, we realized that was unrealistic. The solved strategy not only places pieces in an organized manner but also requires keeping track of the other player’s moves and blocking them when they are about to make a winning move. Keeping track of this many boards and combinations was not feasible in our application, especially without implementing some sort of a search algorithm. In the beginning, we had even hoped to make a Connect 4 game that is flexible with dimensions and board sizes, and initially started with a 7 x 7 board which proved to be extremely difficult to test and run due to the large size. Our compromise was only using a 6 x 7, which is the true size of Connect 4 in real life, that we were eventually able to test by creating 43 boards, which is the most number of boards the game would possibly run for. The large scope of the game made it more difficult to be able to use Forge to compare strategies using forge testing. Therefore, we chose to rely on our visualizations to compare these strategies.
When first defining our project, our final goal was to even explore a 3 dimensional connect 4. We would have loved to explore that, however we were not able to with the time remaining to work on the project. The 3 dimensional Connect 4 would have only been possible with much smaller dimensions and would most likely take longer times to run and test.
For future work, I think one approach we can take on is revisiting our temporal model and fixing the bugs we found there. Despite spending a significant amount of time reviewingand debugging, both in and out of TA hours, we were unable to get it to work. Fixing the temporal model would open up more testing opportunities and allow us to have more concrete comparisons between strategies that we can visualize using our non-temporal model and then run using our temporal model. It would also allow us to implement more complex strategies, as the strategies be programmed to respond to each move more easily.
More future work can also include abstracting the Connect 4 model and allowing it to have more flexible and dynamic board sizes and winning sequences. That would happen through editing our win predicates and well-formed predicates to ensure they can accommodate different row and column sizes that can change according to a user. We would definitely want to improve our win function to use more generalized rules rather than the hardcoded solutions it currently uses.
Future testing regarding strategies can also come in the format of how the same strategy would perform if employed by the first or second player. A lot of strategies of connect 4 are closely tied to who begins the game, therefore, it can be an interesting inquiry to observe when our different strategies can perform most successfully. Other future inquiries would be seeing which of the strategies we employ are more likely to lead to losses, draws, or wins as well.