I model the tic-tac-toe game board this way:
one sig gameBoard {
cells: Row -> Col -> Mark -> Time
}
Mark is either X or O:
enum Mark { X, O }
Row and Col are simply sets:
sig Row {}{ #Row = 3}
sig Col {}{ #Col = 3}
There is a winner when:
I express that with the following complex predicate. Is there a simpler way to express the winner?
pred winner [t: Time] {
some m: Mark |
some r: Row | all c: Col | board[r, c, t] = m
or
some c: Col| all r: Row | board[r, c, t] = m
or
board[first, first, t] = m and
board[first.next, first.next, t] = m and
board[first.next.next, first.next.next, t] = m
or
board[last,last, t] = m and
board[last.prev, last.prev, t] = m and
board[last.prev.prev,last.prev.prev, t] = m
}
Here is my complete tic-tac-toe model:
open util/ordering[Time]
open util/ordering[Row]
open util/ordering[Col]
/*
Structure:
1. The game is played on a 3x3 board.
2. There are two players, Player1 and Player2.
3. Players mark the game board with either X or O.
4. The game is played over a series of time steps.
*/
// 4. The game is played over a series of time steps.
sig Time {}
// 3. Players mark the game board with either X or O.
enum Mark { X, O }
// 2. There are two players, Player1 and Player2.
enum Player { Player1, Player2 }
// 1. The game is played on a ... board.
one sig gameBoard {
cells: Row -> Col -> Mark -> Time
}
// 1. ... on a 3x3 board.
sig Row {}{ #Row = 3}
sig Col {}{ #Col = 3}
/*
Constraints:
1. Each cell has at most one mark (X or O) at each time.
2. A win stops further marking.
3. When all cells are marked, there can be no additional marking.
4. Players alternate moves.
5. There is no interrupt in the play: If cells are empty at time t-1,
and there is no winner at time t-1, then there will be one
fewer empty cells at time t. If there is a winner at time t-1,
then there will be no change to the number of empty cells at
time t (per invariant 2).
6. Player1 marks cells O and Player2 marks cells X.
7. When there is a winner or when all cells are marked,
then the recording of "last player to move" is blank.
*/
// 1. Each cell has at most one mark (X or O) at each time.
pred Each_cell_has_at_most_one_mark {
no r: Row, c: Col, t: Time, disj m, m': Mark |
((r -> c -> m) in gameBoard.cells.t) and
((r -> c -> m') in gameBoard.cells.t)
}
// 2. A win stops further marking.
pred gameBoard_remains_unchanged_after_win {
all t: Time - first |
winner[t.prev] => gameBoard.cells.t = gameBoard.cells.(t.prev)
}
// 3. When all cells are marked, there can be no additional marking.
pred gameBoard_remains_unchanged_after_every_cell_is_marked {
all t: Time - first |
every_cell_is_marked[t.prev] => gameBoard.cells.t = gameBoard.cells.(t.prev)
}
// 4. Players alternate moves.
pred Players_alternately_move {
no t: Time - last, t': t.next |
(some LastPlayerToMove.person.t) and
(some LastPlayerToMove.person.t') and
(LastPlayerToMove.person.t = LastPlayerToMove.person.t')
}
// 5. There is no interrupt in the play: If cells are empty at time t-1,
// and there is no winner at time t-1, then there will be one
// fewer empty cells at time t. If there is a winner at time t-1,
// then there will be no change to the number of empty cells at
// time t (per invariant 2).
pred Progressively_fewer_empty_cells {
all t: Time - first |
not every_cell_is_marked[t.prev] and not winner[t.prev] =>
#empty_cells[t] < #empty_cells[t.prev]
}
// 6. Player1 marks cells O and Player2 marks cells X.
pred Players_mark_cells_appropriately {
all t: Time - first |
not every_cell_is_marked[t.prev] and not winner[t.prev] =>
let c = gameBoard.cells.t - gameBoard.cells.(t.prev) |
c[Row][Col] = X =>
(LastPlayerToMove.person.t = Player2)
else
(LastPlayerToMove.person.t = Player1)
}
// 7. When there is a winner or when all cells are marked,
// then the recording of "last player to move" is blank.
pred LastPlayerToMove_remains_unchanged_after_win_or_all_cells_marked {
all t: Time - first |
((every_cell_is_marked[t.prev]) or (winner[t.prev])) =>
no LastPlayerToMove.person.t
}
// This provides one place that you can call to
// have all the constraints enforced.
pred game_is_constrained_by_these_constraints {
Each_cell_has_at_most_one_mark
gameBoard_remains_unchanged_after_win
gameBoard_remains_unchanged_after_every_cell_is_marked
Players_alternately_move
Progressively_fewer_empty_cells
Players_mark_cells_appropriately
LastPlayerToMove_remains_unchanged_after_win_or_all_cells_marked
}
// Return the set of empty cells at time t.
// This is implemented using set subtraction.
// (Row -> Col) is the set of all possible combinations
// of row and col. Subtract from that the set
// of (row, col) pairs containing a mark at time t.
fun empty_cells[t: Time]: Row -> Col {
(Row -> Col) - gameBoard.cells.t.Mark
}
// Once the game board is completely marked,
// there won't be a "last player." Ditto for when
// there is a winner. That's why there "may" be
// a last player at time t. That is, there isn’t
// necessarily a player involved at every time step,
// i.e., there isn’t necessarily a (Player, Time) pair
// for every value of Time.
one sig LastPlayerToMove {
person: Player lone -> Time
}
// Return the mark (X or O) on board[r][c] at time t,
// or none if there is no mark.
fun board [r: Row, c: Col, t: Time]: lone Mark {
gameBoard.cells[r][c].t
}
// There is a winner when (a) there is a row
// with all X's or all O's, or (b) there is a col
// with all X's or all O's, or (c) there is a left-to-right
// diagonal with all X's or all O's, or (d) there is a
// right-to-left diagonal with all X's or all O's.
pred winner [t: Time] {
some m: Mark |
some r: Row | all c: Col | board[r, c, t] = m
or
some c: Col| all r: Row | board[r, c, t] = m
or
board[first, first, t] = m and
board[first.next, first.next, t] = m and
board[first.next.next, first.next.next, t] = m
or
board[last,last, t] = m and
board[last.prev, last.prev, t] = m and
board[last.prev.prev,last.prev.prev, t] = m
}
// Every call of the game board is marked when
// the set of cells with marks equals all combinations
// of (row, col)
pred every_cell_is_marked[t: Time] {
gameBoard.cells.t.Mark = (Row -> Col)
}
// Initially the game board has no cells.
// One of the players is first to play.
// The game is constrained by the invariants.
pred init [t: Time] {
no gameBoard.cells.t
one p: Player | LastPlayerToMove.person.t = p
game_is_constrained_by_these_constraints
}
pred doNothing [t: Time] {
gameBoard.cells.t = gameBoard.cells.(t.prev)
}
pred Play {
init[first]
all t: Time - first |
X.marked_on_gameboard_at_time[t]
or O.marked_on_gameboard_at_time[t]
or doNothing[t]
}
pred marked_on_gameboard_at_time [m: Mark, t: Time] {
some r: Row, c: Col {
gameBoard.cells.t = gameBoard.cells.(t.prev) +
{r': Row, c': Col, m': Mark | r' = r and c' = c and m' = m}
}
}
run Play for 3 but 12 Time
We design this game around a Board. The Board is the state and we will use game rules encoded in predicates to constrain the transitions to the next board.
Setup the game by defining the board size, the board and the players. The Board has a relative large number of fields because that makes the trace output nice to read.
```alloy
open util/ordering[Board]
let N = 0+1+2
let highest = max[N]
sig Board {
cells : N -> N -> Cell,
move: Cell,
to : N->N,
won : Cell
}
enum Cell { _, X, O }
```
The game is won when there is a row, a colum, or a diagonal that holds the same player. We can encode this as follows:
```alloy
let rightdiag = { r,c : N | r = c }
let leftdiag = { r,c : N | c = highest.minus[r] }
pred won[b,b':Board ] {
some token : X + O {
let positions = b.cells.token {
some row : N | N = row.positions
or some column : N | N = positions.column
or rightdiag in positions
or leftdiag in positions
b'.won = token
}
}
}
```
The game is finished when a player won or there are no more free places.
```alloy
pred finished[ b,b' : Board ] {
not won[b,b'] implies {
b'.won = _
_ not in b'.cells[N][N]
}
b'.cells = b.cells
b'.move = _
b'.to = none -> none
}
```
Plays should alternate between the players. That is why we keep the player in the previous board's move field
and check it is not us. We then constrain the board to have an empty position replaced with the player's
token.
```alloy
pred play[b, b' : Board ] {
b'.won=_
some token : X+O {
b.move != token
b'.move = token
some row,col : N {
b.cells[row][col] = _
b'.cells = b.cells - row->col->_ + row->col->token
b'.to = row->col
}
}
}
```
Then the only thing remaining is to setup the first board and ensure the game (the trace of Boards) is played according to the rules.
```alloy
fact trace {
first.move = _
first.won = _
first.cells = N->N->_
all b' : Board - first, b : b'.prev {
not finished[b,b'] => play[b,b']
}
}
```
With the run we can look for certain types of solutions. In this example we try to find a game where O wins with a righ diagonal ...
```alloy
run { some b : Board | rightdiag in b.cells.(O) } for 11 but 3 int
```
This provides the following output in Alloy 5 Table view (table is reorded from beta 5):
┌──────────┬──────┬────┬───┬───┐
│this/Board│cells │move│to │won│
├──────────┼─┬─┬──┼────┼───┼───┤
│Board⁰ │0│0│_⁰│_⁰ │ │_⁰ │
│ │ ├─┼──┼────┤ ├───┤
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board¹ │0│0│_⁰│X⁰ │2│1│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board² │0│0│_⁰│O⁰ │1│2│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board³ │0│0│_⁰│X⁰ │0│1│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board⁴ │0│0│O⁰│O⁰ │0│0│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board⁵ │0│0│O⁰│X⁰ │2│0│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board⁶ │0│0│O⁰│O⁰ │1│1│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│_⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│O⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board⁷ │0│0│O⁰│X⁰ │1│0│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│O⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
├──────────┼─┼─┼──┼────┼─┬─┼───┤
│Board⁸ │0│0│O⁰│O⁰ │2│2│_⁰ │
│ │ ├─┼──┼────┼─┴─┼───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│O⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
├──────────┼─┼─┼──┼────┼───┼───┤
│Board⁹ │0│0│O⁰│_⁰ │ │O⁰ │
│ │ ├─┼──┼────┤ ├───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│O⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
├──────────┼─┼─┼──┼────┼───┼───┤
│Board¹⁰ │0│0│O⁰│_⁰ │ │O⁰ │
│ │ ├─┼──┼────┤ ├───┤
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│_⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │1│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│O⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
│ ├─┼─┼──┤ │ │ │
│ │2│0│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │1│X⁰│ │ │ │
│ │ ├─┼──┤ │ │ │
│ │ │2│O⁰│ │ │ │
└──────────┴─┴─┴──┴────┴───┴───┘