Primeiras Especificações em TLA+

Slides

1 Correção exercícios

1.1 Correção dos exercícios

Vamos corrigir juntos no VSCode.

  • Mostrar em PDF

2 Modelos em TLA+

2.1 Modelos em TLA+

Até agora, vimos principalmente a parte funcional da linguagem.

  • Diferente de Quint, não temos operadores exclusivos para ações. Ações são bem parecidas com a parte funcional.
  • Podemos identificar ações pelo operador primed (' ), e pelo UNCHANGED

Estado inicial:

  • Em Quint, o estado inicial é uma ação (como x' = 0)
  • Em TLA+, o estado inicial é um predicado (como x = 0, que em Quint seria x==0).
    • Lemos como "Um estado é um estado inicial sse satisfaz \(Init\)"

3 Semáforos

3.1 Especificação para os semáforos

----- MODULE Semaforos ------
EXTENDS Integers, FiniteSets
VARIABLE cores, proximo
CONSTANT SEMAFOROS
\* ...
=============================

PS: Consultei a gramática de TLA+ e precisamos de pelo menos 4 hífens (---- ) antes e depois de MODULE nome e pelo menos 4 iguais (====) no final.

TLAPlusGrammar == \* ...
  G.Module ::= AtLeast4("-")
    & tok("MODULE") & Name & AtLeast4("-")
    & (Nil | (tok("EXTENDS") & CommaList(Name)))
    & (G.Unit)^*
    & AtLeast4("=") \* ...

3.2 Estado inicial

Init ==
  /\ cores = [s \in SEMAFOROS |-> "vermelho"]
  /\ proximo = 0

3.3 Próximo semáforo fica verde

FicaVerde(s) ==
  /\ proximo = s
  /\ \A s2 \in SEMAFOROS : cores[s2] = "vermelho"
  /\ cores' = [cores EXCEPT ![s] = "verde"]
  /\ proximo' = (s + 1) % Cardinality(SEMAFOROS)

Qual a pré-condição dessa ação?

/\ proximo = s
/\ \A s2 \in SEMAFOROS : cores[s2] = "vermelho"

3.4 Próximo semáforo fica verde: Exercício

FicaVerde(s) ==
  /\ proximo = s
  /\ \A s2 \in SEMAFOROS : cores[s2] = "vermelho"
  /\ cores' = [cores EXCEPT ![s] = "verde"]
  /\ proximo' = (s + 1) % Cardinality(SEMAFOROS)

Lendo essa ação: tente prencher as lacunas
"FicaVerde para um semáforo s define uma transição onde, no estado atual, __________ deve ser __________ e ___________ deve _________; e no próximo estado, _________ deve ser _________ e ___________ deve ser ___________"

3.5 Próximo semáforo fica verde: Exercício

FicaVerde(s) ==
  /\ proximo = s
  /\ \A s2 \in SEMAFOROS : cores[s2] = "vermelho"
  /\ cores' = [cores EXCEPT ![s] = "verde"]
  /\ proximo' = (s + 1) % Cardinality(SEMAFOROS)

Possível resolução:
"FicaVerde para um semáforo s define uma transição onde, no estado atual, o valor de proximo deve ser igual ao semáforo s e o valor de cores para cada semáforo em SEMAFOROS deve ser vermelho; e no próximo estado, o valor de cores deve ser igual a cores no estado atual, exceto que o valor de s deve ser verde e o valor de proximo deve ser o incremento do valor no estado atual módulo o tamanho do conjunto SEMAFOROS".

3.6 Um semáforo que está verde fica amarelo

FicaAmarelo(s) ==
  /\ cores[s] = "verde"
  /\ cores' = [cores EXCEPT ![s] = "amarelo"]
  /\ UNCHANGED << proximo >>

Qual a pré-condição dessa ação?

cores[s] = "verde"

3.7 Um semáforo que está amarelo fica vermelho

FicaVermelho(s) ==
  /\ cores[s] = "amarelo"
  /\ cores' = [cores EXCEPT ![s] = "vermelho"]
  /\ UNCHANGED << proximo >>

Qual a pré-condição dessa ação?

cores[s] = "amarelo"

3.8 Função de próximo estado

Next == \E s \in SEMAFOROS : FicaVerde(s) \/ FicaAmarelo(s) \/ FicaVermelho(s)

Lembrando que TLA+ permite usarmos ações dentro de um exists, diferentemente de Quint onde é necessário usar o nondet e oneOf.

3.9 Propriedades

Uma invariante para check de sanidade:

Inv == cores[2] /= "amarelo"

Uma propriedade do sistema: para que os veículos não colidam, não podemos ter mais de um semáforo aberto ao mesmo tempo.

SemColisao == Cardinality({s \in SEMAFOROS : cores[s] = "verde"}) <= 1

4 Jogo da Velha

4.1 Jogo da Velha em TLA+

Vamos ver a mesma especificação do jogo da velha, agora em TLA+

  • Vamos direto pra versão onde o jogador X usa estratégia
  • Vou usar a versão original do autor (SWART, 2022)
    • A especificação em Quint é baseada nesta, mas não é uma tradução direta. Poderíamos escrever a tradução mais próxima possível, mas não é esse o caso. Eu escrevi como achei que seria melhor, dado os recursos da linguagem.

4.2 Módulo

-------- MODULE tictactoexwin ---------

EXTENDS Naturals

\* ...

=======================================

4.3 Tipos e variáveis

Definimos as seguintes variáveis

VARIABLES
  board, \* board[1..3][1..3] A 3x3 tic-tac-toe board
  nextTurn \* who goes next

4.4 Definições sobre coordenadas e tabuleiro

BoardIs(coordinate, player) ==
    board[coordinate[1]][coordinate[2]] = player

BoardFilled ==
    \* There does not exist
    ~\E i \in 1..3, j \in 1..3:
        \* an empty space
        LET space == board[i][j] IN
        space = "_"

BoardEmpty ==
    \* There does not exist
    \A i \in 1..3, j \in 1..3:
        \* an empty space
        LET space == board[i][j] IN
        space = "_"

4.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 tuplas! Na implementação em Quint, usamos filter e size para ver se um pattern tinha dois X e um branco, um X e dois brancos, etc. Aqui, o autor usa listas de permutação.
WinningPositions == {
    \* Horizonal wins
    <<<<1,1>>, <<1,2>>, <<1,3>>>>,
    <<<<2,1>>, <<2,2>>, <<2,3>>>>,
    <<<<3,1>>, <<3,2>>, <<3,3>>>>,
    \* Vertical wins
    <<<<1,1>>, <<2,1>>, <<3,1>>>>,
    <<<<1,2>>, <<2,2>>, <<3,2>>>>,
    <<<<1,3>>, <<2,3>>, <<3,3>>>>,
    \* Diagonal wins
    <<<<1,1>>, <<2,2>>, <<3,3>>>>,
    <<<<3,1>>, <<2,2>>, <<1,3>>>>
}

4.6 Definindo "ganhar" - operador won

Usamos a definição winningPositions para determinar se um jogador venceu.

Won(player) ==
    \* A player has won if there exists a winning position
    \E winningPosition \in WinningPositions:
        \* Where all the needed spaces
        \A i \in 1..3:
            \* are occupied by one player
            board[winningPosition[i][1]][winningPosition[i][2]] = player

4.7 Ações - Move

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

  • Determinístico
Move(player, coordinate) ==
    /\ board[coordinate[1]][coordinate[2]] = "_"
    /\ board' = [board EXCEPT
                        ![coordinate[1]][coordinate[2]] = player]

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

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

4.8 Ações - MoveToEmpty

Um dado jogador faz uma jogada em alguma coordenada

  • Não-determinístico
MoveToEmpty(player) ==
  /\ \E i \in 1..3: \E j \in 1..3: \* There exists a position on the board
    /\ board[i][j] = "_" \* Where the board is currently empty
    /\ Move(player, <<i,j>>)

  • 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

  • Aonde temos não determinismo aqui?

    • No uso da ação Move, que atualiza a variável board dentro de um exists (\E).

4.9 Ações - MoveO

MoveO ==
  /\ nextTurn = "O" \* Only enabled on O's turn
  /\ ~Won("X") \* And X has not won
  /\ MoveToEmpty("O") \* O still tries every empty space
  /\ nextTurn' = "X" \* The future state of next turn is X

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

    /\ nextTurn = "O" \* Only enabled on O's turn
/\ ~Won("X") \* And X has not won
    • Implicitamente, também temos a pré-condição de MoveToEmpty empregada nessa ação

4.10 Estratégia para o jogador X

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

4.11 Começando com os cantos

Corners == {
    <<1,1>>,
    <<3,1>>,
    <<1,3>>,
    <<3,3>>
}

StartInCorner ==
    \E corner \in Corners:
        Move("X", corner)

4.12 Condições para as jogadas

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

Para isso, nessa especificação, definimos as permutações, e fazemos um nível a mais de interação (com exists), verificando, para cada winningPosition e para cada permutação, se aquela permutação da winningPosition é uma ordem específica do que queremos (X, X, e vazio).

PartialWins == {
    <<1,2,3>>,
    <<2,3,1>>,
    <<3,1,2>>
}
CanWin == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]],"X")
  /\ BoardIs(winningPostion[partialWin[2]],"X")
  /\ BoardIs(winningPostion[partialWin[3]],"_")

CanBlockWin == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]], "O")
  /\ BoardIs(winningPostion[partialWin[2]], "O")
  /\ BoardIs(winningPostion[partialWin[3]], "_")

CanTakeCenter == board[2][2] = "_"

CanSetupWin == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]], "X")
  /\ BoardIs(winningPostion[partialWin[2]], "_")
  /\ BoardIs(winningPostion[partialWin[3]], "_")

4.13 Ações - Win

Win == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]],"X")
  /\ BoardIs(winningPostion[partialWin[2]],"X")
  /\ BoardIs(winningPostion[partialWin[3]],"_")
  /\ Move("X", winningPostion[partialWin[3]])
  • Qual é a pré-condição pra essa ação?
\E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]],"X")
  /\ BoardIs(winningPostion[partialWin[2]],"X")
  /\ BoardIs(winningPostion[partialWin[3]],"_")
  • Percebam que essa pré condição é exatamente CanWin
  • Porém, não conseguimos usar CanWin aqui porque precisamos saber em qual posição jogar.

4.14 Ações - BlockWin

De forma semelhante, BlockWin:

BlockWin == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]], "O")
  /\ BoardIs(winningPostion[partialWin[2]], "O")
  /\ BoardIs(winningPostion[partialWin[3]], "_")
  /\ Move("X", winningPostion[partialWin[3]])

4.15 Ações - TakeCenter e SetupWin

TakeCenter ==
    /\ Move("X", <<2,2>>)

SetupWin == \E winningPostion \in WinningPositions, partialWin \in PartialWins:
  /\ BoardIs(winningPostion[partialWin[1]], "X")
  /\ BoardIs(winningPostion[partialWin[2]], "_")
  /\ BoardIs(winningPostion[partialWin[3]], "_")
  /\ \E i \in 2..3:
    Move("X", winningPostion[partialWin[i]])

4.16 Ações - MoveX

MoveX ==
    /\ nextTurn = "X" \* Only enabled on X's turn
    /\ ~Won("O") \* And X has not won
    \* This specifies the spots X will move on X's turn
    /\ \/ /\ BoardEmpty
          /\ StartInCorner
       \/ /\ ~BoardEmpty \* If its not the start
          /\ \/ /\ CanWin
                /\ Win
             \/ /\ ~CanWin
                /\  \/ /\ CanBlockWin
                       /\ BlockWin
                    \/ /\ ~CanBlockWin
                       /\ \/ /\ CanTakeCenter
                             /\ TakeCenter
                          \/ /\ ~CanTakeCenter
                             /\ \/ /\ CanSetupWin
                                   /\ SetupWin
                                \/ /\ ~CanSetupWin
                                  /\ MoveToEmpty("X") \* No more strategies. Pick spot
    /\ nextTurn' = "O" \* The future state of next turn is O

4.17 Estado inicial

Init ==
  /\ nextTurn = "X" \* X always goes first
  \* Every space in the board states blank
  /\ board = [i \in 1..3 |-> [j \in 1..3 |-> "_"]]

4.18 Transições

GameOver == Won("X") /\ Won("O") /\ BoardFilled

\* Every state, X will move if X's turn, O will move on O's turn
Next == MoveX \/ MoveO \/ (GameOver /\ UNCHANGED << board, nextTurn >>)
  • Nota: isso está um pouco diferente na especificação original, porque o autor usa a definição de Spec ao invés de somente Init e Next.
\* Every state, X will move if X's turn, O will move on O's turn
Next == MoveX \/ MoveO

\* A description of every possible game of tic-tac-toe
\* will play until the board fills up, even if someone won
Spec == Init /\ [][Next]_<<board,nextTurn>>

4.19 Invariantes

XHasNotWon == ~Won("X")
OHasNotWon == ~Won("O")

\* It's not a stalemate if one player has won or the board is not filled
NotStalemate ==
    \/ Won("X")
    \/ Won("O")
    \/ ~BoardFilled

4.20 Referências

SWART, E. Introduction to pragmatic formal modeling. Disponível em: <https://elliotswart.github.io/pragmaticformalmodeling/>.