Can somebody explain what is going on? And what techniques can be used to fix this?
I get the feeling that recursion in TLA+ works differently compared to regular programming languages and that I'm missing something.
Thanks,
------------------------------- MODULE tictactoe -------------------------------
EXTENDS Integers
N == 2
Players == {"X", "O"}
Tiles == (0..N) \X (0..N)
Token == {" ", "X", "O"}
Board == [Tiles -> Token]
VARIABLES board, turn
vars == <<board, turn>>
NextPlayer == [X |-> "O", O |-> "X"]
ThreeInARow(B, T) ==
\/ \E x \in 0..N: \A y \in 0..N: (B[<<x, y>>] = T \/ B[<<y, x>>] = T)
\/ \A x \in 0..N: B[<<x, x>>] = T
\/ \A x \in 0..N: B[<<x, N-x>>] = T
Win(B) == ThreeInARow(B, "X")
Lose(B) == ThreeInARow(B, "O")
Draw(B) == ~Win(B) /\ ~Lose(B) /\ \A t \in Tiles: B[t] /= " "
Done == Draw(board) \/ Win(board) \/ Lose(board)
PossibleMoves(B) == {x \in Tiles: B[x] = " "}
RECURSIVE GoodMove(_, _)
GoodMove(B, M) ==
LET B_0 == [B EXCEPT ![M] = "X"] IN
IF Win(B) \/ Draw(B)
THEN TRUE
ELSE \A counter \in PossibleMoves(B_0):
LET B_1 == [B_0 EXCEPT ![counter] = "O"] IN
\E y \in PossibleMoves(B_1): GoodMove(B_1, y)
Move ==
/\ turn' = NextPlayer[turn]
/\ \E x \in PossibleMoves(board):
/\ board' = [board EXCEPT ![x] = turn]
/\ turn = "X" => GoodMove(board, x) \* Comment out this line for all possible games and no stack overflow
Init ==
/\ board = [t \in Tiles |-> " "]
/\ turn = "X"
Next ==
\/ ~Done /\ Move
\/ Done /\ UNCHANGED vars
Fairness == WF_vars(Move)
Spec == Init /\ [][Next]_vars /\ Fairness
TypeInvariant ==
/\ turn \in Players
/\ board \in Board
_OneOutcomeInvariant_ ==
/\ Win(board) => (~Lose(board) /\ ~Draw(board))
/\ Lose(board) => (~Win(board) /\ ~Draw(board))
/\ Draw(board) => (~Lose(board) /\ ~Win(board))
TerminationInvariant == <>[] Done
CanWinContradiction == []~Win(board)
CanLoseContradiction == []~Lose(board)
CanDrawContradiction == []~Draw(board)
=============================================================================