Vamos corrigir juntos no VSCode.
Até agora, vimos principalmente a parte funcional da linguagem.
' ), e pelo UNCHANGED
Estado inicial:
x' = 0)x = 0, que em Quint seria x==0).----- 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("=") \* ...
Init == /\ cores = [s \in SEMAFOROS |-> "vermelho"] /\ proximo = 0
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"
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 ___________”
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”.
FicaAmarelo(s) == /\ cores[s] = "verde" /\ cores' = [cores EXCEPT ![s] = "amarelo"] /\ UNCHANGED << proximo >>
Qual a pré-condição dessa ação?
cores[s] = "verde"
FicaVermelho(s) == /\ cores[s] = "amarelo" /\ cores' = [cores EXCEPT ![s] = "vermelho"] /\ UNCHANGED << proximo >>
Qual a pré-condição dessa ação?
cores[s] = "amarelo"
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.
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
Vamos ver a mesma especificação do jogo da velha, agora em TLA+
-------- MODULE tictactoexwin --------- EXTENDS Naturals \* ... =======================================
Definimos as seguintes variáveis
VARIABLES board, \* board[1..3][1..3] A 3x3 tic-tac-toe board nextTurn \* who goes next
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 = "_"
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>>>>
}
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
Um dado jogador faz uma jogada (um move) em uma dada coordenada
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?
Um dado jogador faz uma jogada em alguma coordenada
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?
Aonde temos não determinismo aqui?
Move, que atualiza a variável board dentro de um exists (\E).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
MoveToEmpty empregada nessa ação
Estratégia:
Corners == {
<<1,1>>,
<<3,1>>,
<<1,3>>,
<<3,3>>
}
StartInCorner ==
\E corner \in Corners:
Move("X", corner)
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]], "_")
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]])
\E winningPostion \in WinningPositions, partialWin \in PartialWins: /\ BoardIs(winningPostion[partialWin[1]],"X") /\ BoardIs(winningPostion[partialWin[2]],"X") /\ BoardIs(winningPostion[partialWin[3]],"_")
CanWinCanWin aqui porque precisamos saber em qual posição jogar.
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]])
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]])
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
Init == /\ nextTurn = "X" \* X always goes first \* Every space in the board states blank /\ board = [i \in 1..3 |-> [j \in 1..3 |-> "_"]]
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 >>)
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>>
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