Modelling TicTacToe in Alloy

Question

How do I write a predicate to check for a Horizontal, vertical or diagonal wins for a tictactoe game in Alloy? I'm kind of struggling with the syntax below is my code:

open util/ordering [Time] as T

sig Time {}

abstract sig Game {
  turn, winner, loser: Game
}

abstract sig Player {
  opponent:Player
}

sig X extends Player {}
sig O extends Player {}

fact {  
  all t:Time| all p: Player | no p.opponent
  all t: Time | all p: Player | all g:Game | one g.turn
  all t:Time | all g:Game | one g.winner & g.loser
} 

pred HorizontalWin {

}

Answer 1

I think your model might not be appropriate for this game. For example, I don't see a 3x3 grid in your model, so it is not clear how to express any property about the state of the game.

There are several other issues with your model. For example, the Game sig is abstract and it has no concrete subsigs, so instances of this model can never contain any games (thus turn, winner, and loser fields will always be empty as well). Also, you probably want to use the Time signature somewhere (either put some fields in it, or make other fields use it, e.g., turn: Player -> Time) and then add some facts about every two consecutive time steps to properly connect the game moves. Here is an idea:

open util/ordering [Move] as M

abstract sig Player {}
one sig X, O extends Player {}

abstract sig Cell {}
one sig C00, C01, C02, C10, C11, C12, C20, C21, C22 extends Cell {}

sig Board {
  grid: Cell -> lone Player
} 

sig Move {
  player: Player,
  pos: Cell,
  board, board': Board // pre and post board
} {
  // must choose an empty grid cell
  no board.grid[pos]
  // set the `pos` cell to `player`
  board'.grid[pos] = player
  // all other grid cells remain the same
  all c: Cell - pos | board'.grid[c] = board.grid[c]
}

fact {
  // empty board at the beginning
  no M/first.board.grid
  all m: Move {
    some M/next[m] => {
      // alternate players each move
      M/next[m].player != m.player
      // connect boards
      M/next[m].board = m.board'
    }
  }
}


run {} for 9 but 10 Board