1.1 Jogo da Velha

Todos conhecem jogo da velha?

PS: a partir de hoje, não vou mais traduzir as especificações para português

• Acho legal usar português no início para que fique claro o que são keywords (sempre em inglês) e o que podemos escolher o nome (nesses casos, em português)
  
• A partir daqui, vou usar os exemplos originais, em inglês.

1.2 Tipos e variáveis

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

1.3 Definições sobre coordenadas

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
  }

1.4 Definições sobre o tabuleiro

val boardEmpty = boardCoordinates.forall(isEmpty)

val boardFull = not(boardCoordinates.exists(isEmpty))

1.5 Definindo "ganhar" - coordenadas

• Como o tabuleiro é sempre 3x3, é mais fácil listar todas as combinações de coordenadas que levam a uma vitória do que implementar os cálculos.
  
• Usamos 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))
)

1.6 Definindo "ganhar" - operador won

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

• Reparem que o operador or pode ser usado na forma infixa (no meio dos argumentos)

1.7 Ações - Move

Um dado jogador faz uma jogada (um move) em uma dada coordenada

• Determinístico
  

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?

  • A pré-condição para essa ação é que a coordenada esteja vazia
    

• setBy é bem útil pra atualizar mapas aninhados (como nesse caso, int -> int -> Square)

1.8 Ações - MoveToEmpty

Um dado jogador faz uma jogada em alguma coordenada

• Não-determinístico
  

action MoveToEmpty(player) = all {
  not(gameOver),
  nondet coordinate = boardCoordinates.filter(isEmpty).oneOf()
  Move(player, coordinate)
}

• Qual é a pré-condição pra essa ação?

  • A pré-condição para essa ação é que o jogo ainda não tenha acabado

1.9 Ações - MoveO e MoveX

• Por enquanto, as ações 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.

1. Move0

   action MoveO = all {
     nextTurn == O,
     MoveToEmpty(O),
     nextTurn' = X,
   }
   

2. MoveX

   action MoveX = all {
     nextTurn == X,
     MoveToEmpty(X),
     nextTurn' = O,
   }
   

3. B_ignoreheading

   • Qual é a pré-condição pra essas ações?

     • Para ambas, a pré-condição é que seja o turno do jogador a fazer a jogada
       • Implicitamente, também temos a pré-condição de MoveToEmpty empregada nessa ação

1.10 Estado inicial

action 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)),
}

1.11 Transições

action step = any {
  MoveX,
  MoveO,
  // If the game is over, we don't need to do anything
  all { gameOver, board' = board, nextTurn' = nextTurn },
}

1.12 Rodando jogos aleatórios com o simulador

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
}

1.13 Usando uma invariante para procurar jogos que "dão velha"

"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

1.14 Contraexemplo

[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
}

2.1 Jogando pra ganhar

• Jogo da velha é um jogo bem simples e fácil
  
• Ainda quando crianças, enjoamos do jogo, porque percebemos que "sempre dá velha"
  
• Hipótese: Se um jogador seguir uma certa estratégia, ele nunca perde.
  • Consequência: Se os dois jogadores seguirem essa estratégia, nenhum dos dois perde - "sempre dá velha"

Estratégia:

• A primeira jogada é sempre nos cantos
  
• As outras jogadas fazem a primeira jogada possível nessa lista de prioridade:
  • Ganhar
    
  • Bloquear
    
  • Jogar no centro
    
  • Preparar uma vitória (preenchendo 2 de 3 quadrados numa fila/coluna/diagonal)
    
  • Jogada qualquer

Vamos implementar essa estratégia para o jogador X, enquanto o jogador O continua jogando "de qualquer jeito".

2.2 Começando com os cantos

pure val corners = Set(
  (1,1),
  (3,1),
  (1,3),
  (3,3)
)

action StartInCorner =
  nondet corner = oneOf(corners)
  Move(X, corner)

2.3 Condições para as jogadas

Precisamos definir as condições que determinam se cada uma das jogadas na lista de prioridade pode ser feita.

• Ganhar
  
• Bloquear
  
• Jogar no centro
  
• Preparar uma vitória

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)

2.4 Condições para as jogadas - definições auxiliares

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,
}

2.5 Ações - Win

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)
    

  • Isso é importante para garantir que nunca estamos chamando oneOf em um set vazio.

2.6 Ações - Block

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.

• Não existe algo como "pegar o primeiro elemento do set" - porque sets não são ordenados!

2.7 Ações - TakeCenter e SetupWin

action TakeCenter = Move(X, (2, 2))

action SetupWin = all {
  nondet pattern = winningPatterns.filter(canSetupWinWithPattern).oneOf()
  nondet coordinate = pattern.filter(isEmpty).oneOf()
  Move(X, coordinate),
}

2.8 Ações - alterando MoveX

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,
}

2.9 Invariantes

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))

2.10 Fórmulas temporais

/// This is not always true, as if O picks the right moves, the game will
/// result in a stalemate.
temporal XMustEventuallyWin = eventually(won(X))

• Infelizmente, a implementação de propriedades temporais no Apalache ainda é bem rudimentar.
  
• Podemos traduzir Quint pra TLA+ e usar o TLC para checar essa propriedade
  • Existe um script para chamar o TLC com os parâmetros apropriados, que podemos usar enquanto a integração não está pronta
    • sh tlc/check_with_tlc.sh --file tictactoe.qnt --temporal XMustEventuallyWin
      
• O simulador não suporta fórmulas temporais
  • Poderia suportar parcialmente com aquela implementação que fizemos em C++/Haskell na disciplina

2.11 Tarefa de casa

Tarefa para a próxima aula: ler o blogpost https://elliotswart.github.io/pragmaticformalmodeling/

• Serve como uma revisão de alguns conteúdos da matéria até agora
  
• Explica a modelagem do jogo da velha em TLA+, que veremos na próxima aula
  
• Também conta como referência pra essa aula :)

2.12 FIM