# [tlaplus] Recursion without StackOverflowError

Hi,

Looked around online for a TLA+ community and this looks like the best place for a beginner to ask some questions.

I'm trying to model tic-tac-toe with the end goal to show that the starting player doesn't have to lose.

I started with a specification that has all possible game states, and did some sanity checks on it. This all worked as expected.

Next I wanted to show than by restricting the moves of the first player to "good moves" that the system doesn't deadlock and Lose(board) is unreachable.

I wrote a recursive function GoodMove() that tries to ensure that after every counter move there is still a good move to make. Resulting in a Win or a Draw.

However with this addition TLC crashes with an java.lang.StackOverflowError. I understand that recursion can result in a stack overflow, but the recursion in this case should be bounded. Each iteration sets a tile, and at one point all tiles are set and this must be a Win or a Draw. So I don't understand why this results in a stack overflow.

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