Recursion without StackOverflowError

[Isaac Dynamo]

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

CanWinContradiction  == []~Win(board)
CanLoseContradiction == []~Lose(board)
CanDrawContradiction == []~Draw(board)

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

[Markus Kuppe]

Hi Isaac,

you have identified a bug in TLC's handling of lazy values within the
scope of ENABLED combined with recursion:
https://github.com/tlaplus/tlaplus/issues/991. TLC only throws a
StackOverflowError if it verifies the TerminationInvariant property.
To work around the bug when checking the property, wrap the recursive
call to GoodMove within TLCEval (defined in the TLC module).


EXTENDS Integers, TLC

[...]

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): TLCEval(GoodMove(B_1, y))


Markus