Alloy practice problem: Tic Tac Toe

One of my friends was recently interviewing and was asked to create an API for tic tac toe. As far as interview questions go it seems like a reasonable problem for demonstrating programming understanding but I want to one-up the interviewers by solving the game in Alloy.

I’m going to assume everyone knows the game but even if you don’t I’ll explain it as I elaborate the model.

The evolution of the game is going to consist of states

The game itself happens on a 3×3 board which we are going to model as a matrix with rows and columns

The game has two players which are identified with the marks they are allowed to place on the board

The game board itself consists of marked rows and columns. Since we have identified the marks with the players the signature for the board is a pretty simple mapping from row/column pairs to players with the restriction that two players can’t mark the same row/column pair

The state itself consists of a board and the player that is going to make the next mark on the board

We are done with the fundamental building blocks and restrictions and can now define the transition relation which encodes the rules of the game

The comments explain what is going on but to unpack it a bit more: if a player is about to make a mark then in the next state it can’t be allowed to make a mark again, the cells from the previous state must be in the next state, we don’t tamper with the moves of the previous player when the current player is making a mark (think about what happens if this restriction is removed), the next state contains only 1 extra mark and it is a mark by the current player.

The only other thing we need to specify is the winning condition

Again I think the comments explain it but to unpack it: if the player occupies a row or a column or one of the diagonals then that player is winning.

With all of the above we can run the model and find some winning state transitions for player X