Todos conhecem jogo da velha?
PS: a partir de hoje, não vou mais traduzir as especificações para português
keywords (sempre em inglês) e o que podemos escolher o nome (nesses casos, em português)
Definimos os seguintes tipos
type Player = X | O type Square = Occupied(Player) | Empty
E as seguintes variáveis
/// A 3x3 tic-tac-toe board var board: int -> int -> Square /// Who goes next var nextTurn: Player
pure val boardCoordinates = tuples(1.to(3), 1.to(3)) def square(coordinate: (int, int)): Square = board.get(coordinate._1).get(coordinate._2) def hasPlayer(coordinate, player) = match square(coordinate) { | Empty => false | Occupied(p) => player == p } def isEmpty(coordinate) = match square(coordinate) { | Empty => true | _ => false }
val boardEmpty = boardCoordinates.forall(isEmpty) val boardFull = not(boardCoordinates.exists(isEmpty))
Set - não precisamos de ordem nem de repetição, logo não devemos usar List.pure val winningPatterns = Set( // Horizonal wins Set((1,1), (1,2), (1,3)), Set((2,1), (2,2), (2,3)), Set((3,1), (3,2), (3,3)), // Vertical wins Set((1,1), (2,1), (3,1)), Set((1,2), (2,2), (3,2)), Set((1,3), (2,3), (3,3)), // Diagonal wins Set((1,1), (2,2), (3,3)), Set((3,1), (2,2), (1,3)) )
Usamos as definições para winningPaterns e hasPlayer para determinar se um jogador venceu.
def won(player) = winningPatterns.exists(pattern =>
pattern.forall(coordinate => hasPlayer(coordinate, player))
)
Com essa definição e boardFull, podemos determinar se um jogo já acabou.
val gameOver = won(X) or won(O) or boardFull
or pode ser usado na forma infixa (no meio dos argumentos)
Um dado jogador faz uma jogada (um move) em uma dada coordenada
action Move(player, coordinate) = all { isEmpty(coordinate), board' = board.setBy( coordinate._1, row => row.set(coordinate._2, Occupied(player)) ), }
Qual é a pré-condição pra essa ação?
setBy é bem útil pra atualizar mapas aninhados (como nesse caso, int -> int -> Square)
Um dado jogador faz uma jogada em alguma coordenada
action MoveToEmpty(player) = all { not(gameOver), nondet coordinate = boardCoordinates.filter(isEmpty).oneOf() Move(player, coordinate) }
Qual é a pré-condição pra essa ação?
MoveO e MoveX são bem parecidas porque ambos jogam “de qualquer jeito”. Não vamos parametrizar elas porque depois vamos mudar somente o comportamento de X.action MoveO = all { nextTurn == O, MoveToEmpty(O), nextTurn' = X, }
action MoveX = all { nextTurn == X, MoveToEmpty(X), nextTurn' = O, }
Qual é a pré-condição pra essas ações?
MoveToEmpty empregada nessa açãoaction init = all { // X always goes first nextTurn' = X, // Every space in the board starts blank board' = 1.to(3).mapBy(_ => 1.to(3).mapBy(_ => Empty)), }
action step = any { MoveX, MoveO, // If the game is over, we don't need to do anything all { gameOver, board' = board, nextTurn' = nextTurn }, }
quint run tictactoe.qnt --max-samples=1
...
[State 20]
{
board:
Map(
1 -> Map(1 -> Occupied(O), 2 -> Occupied(X), 3 -> Occupied(X)),
2 -> Map(1 -> Occupied(X), 2 -> Occupied(O), 3 -> Occupied(O)),
3 -> Map(1 -> Occupied(X), 2 -> Occupied(O), 3 -> Occupied(X))
),
nextTurn: O
}
“Dar velha”, ou stalemate, quer dizer que o tabuleiro está cheio e ninguém ganhou. É um empate.
val stalemate = boardFull and not(won(X)) and not(won(O)) val NotStalemate = not(stalemate)
Essa invariante é fácil de quebrar, podemos usar o simulador ao invés do model checker tranquilamente:
quint run tictactoe.qnt --invariant=NotStalemate
Mas podemos usar o model checker também! Ele vai demorar mais, porque faz BFS e vai levar um tempo para chegar em jogos com 9 jogadas feitas, que são necessárias para um tabuleiro completo.
quint verify tictactoe.qnt --invariant=NotStalemate
[State 9]
{
board:
Map(
1 -> Map(1 -> Occupied(O), 2 -> Occupied(X), 3 -> Occupied(O)),
2 -> Map(1 -> Occupied(O), 2 -> Occupied(X), 3 -> Occupied(X)),
3 -> Map(1 -> Occupied(X), 2 -> Occupied(O), 3 -> Occupied(X))
),
nextTurn: O
}
Estratégia:
Vamos implementar essa estratégia para o jogador X, enquanto o jogador O continua jogando “de qualquer jeito”.
pure val corners = Set( (1,1), (3,1), (1,3), (3,3) ) action StartInCorner = nondet corner = oneOf(corners) Move(X, corner)
Precisamos definir as condições que determinam se cada uma das jogadas na lista de prioridade pode ser feita.
val canWin = winningPatterns.exists(canWinWithPattern) val canBlock = winningPatterns.exists(canBlockWithPattern) val canTakeCenter = isEmpty((2,2)) val canSetupWin = winningPatterns.exists(canSetupWinWithPattern)
(canWinWithPattern, canBlockWithPattern e canSetupWintWithPattern a seguir)
Dado um winning pattern, podemos ganhar com aquele pattern sse duas das coordenadas tiverem X e a outra estiver vazia. Lembrando que a ordem não importa.
def canWinWithPattern(pattern) = and { pattern.filter(coordinate => coordinate.hasPlayer(X)).size() == 2, pattern.filter(coordinate => coordinate.isEmpty()).size() == 1, }
Dado um winning pattern, podemos bloquear com aquele pattern sse duas das coordenadas tiverem O e a outra estiver vazia.
def canBlockWithPattern(pattern) = and { pattern.filter(coordinate => coordinate.hasPlayer(O)).size() == 2, pattern.filter(coordinate => coordinate.isEmpty()).size() == 1, }
Dado um winning pattern, podemos preparar uma vitória com aquele pattern sse uma das coordenadas tiver X e as outras duas estiverem vazias.
def canSetupWinWithPattern(pattern) = and { pattern.filter(coordinate => coordinate.hasPlayer(X)).size() == 1, pattern.filter(coordinate => coordinate.isEmpty()).size() == 2, }
action Win = all { canWin, nondet pattern = winningPatterns.filter(canWinWithPattern).oneOf() nondet coordinate = pattern.filter(isEmpty).oneOf() Move(X, coordinate), }
Qual é a pré-condição pra essa ação?
canWin, lembrando que canWin é definido por: val canWin = winningPatterns.exists(canWinWithPattern)
oneOf em um set vazio.action Block = all { canBlock, nondet pattern = winningPatterns.filter(canBlockWithPattern).oneOf() nondet coordinate = pattern.filter(isEmpty).oneOf() Move(X, coordinate), }
Observem o uso de oneOf para selecionar a coordenada aqui. Nesses casos (tanto Win quanto Block), essa seleção é determinística, porque sabemos que sempre haverá uma única coordenada vazia nesses patterns. Contudo, o Quint não sabe disso.
action TakeCenter = Move(X, (2, 2)) action SetupWin = all { nondet pattern = winningPatterns.filter(canSetupWinWithPattern).oneOf() nondet coordinate = pattern.filter(isEmpty).oneOf() Move(X, coordinate), }
Temos todas as ações para a estratégia definidas, agora basta definir um novo MoveX que chama essas ações conforme a prioridade estabelecida.
action MoveX = all { nextTurn == X, if (boardEmpty) StartInCorner else if (canWin) Win else if (canBlock) Block else if (canTakeCenter) TakeCenter else if (canSetupWin) SetupWin else MoveToEmpty(X), nextTurn' = O, }
Com isso, temos nosso modelo. Agora, vamos definir algumas invariantes para o uso dessa estratégia.
/// X has not won. This does not hold, as X wins most of the times. val XHasNotWon = not(won(X)) /// O has not won. This should hold, as O can only achieve a draw. val OHasNotWon = not(won(O))
/// This is not always true, as if O picks the right moves, the game will /// result in a stalemate. temporal XMustEventuallyWin = eventually(won(X))
Tarefa para a próxima aula: ler o blogpost https://elliotswart.github.io/pragmaticformalmodeling/