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

[Hillel Wayne]

Generally when doing these kinds of recursive things, I find it easier to generate all possible values as a value, instead of as a computation. There are only 3^9 (19683) possible tic-tac-toe boards. This means you can do things like

GoodBoard[B \in Board] ==

  IF Win(B) \/ Draw(B)
            THEN TRUE

            ELSE \A B_1 \in {[B_0 EXCEPT ![counter] = "O"]: counter \in PossibleMoves(B_0)]}:
                    \E y \in PossibleMoves(B_1): GoodBoard(B_1)

I think this will make TLC generate the whole function as one value and avoid a stackoverflow error. See Specifying Systems 6.4 for the trick of using "Function Definitions" to make recursive functions.

H

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5edb0bb5-a335-4518-88a3-dee7fb9b9d05n%40googlegroups.com.

[Isaac Dynamo]

Hi Markus,

Your suggested workaround works great. And after fixing some of my own bugs in the GoodMove() function, I think I was able to show that first player never has to lose a game.

Thanks for your help!

Isaac

Op zondag 21 juli 2024 om 19:09:27 UTC+2 schreef Markus Kuppe:

[Markus Kuppe]

FYI: The Github issue https://github.com/tlaplus/tlaplus/issues/991 includes a second workaround in addition to the technical analysis.

M.

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e890b810-5fcf-482b-8c9b-0316bddded91n%40googlegroups.com.

[Isaac Dynamo]

Interesting. Gravitated to the RECURSIVE approach because it looked familiair, but it felt a bit bad that I wasn't expressing it with memoization. But maybe that TLC already uses memoization internally for functions?

After reading the reference and surrounding sections, I think that I now also have a better understanding of CHOOSE. Maybe the time has come to read it completely, instead of diving in head first and messing around.

Tried to update the model with your approach, and ended up with this:

GoodBoard[B_0 \in Board] ==
    IF Win(B_0) \/ Draw(B_0) THEN TRUE
    ELSE \A B_1 \in {[B_0 EXCEPT ![counter] = "O"]: counter \in PossibleMoves(B_0)}:
        IF Lose(B_1) THEN FALSE
        ELSE \E B_2 \in {[B_1 EXCEPT ![y] = "X"]: y \in PossibleMoves(B_1)}:
            GoodBoard[B_2]

Unfortunately this fails to terminate within 10sec. Maybe this is because the recursion doesn't visit all boards due the "short circuiting" on Win, Draw or Lose. 

However I'm still a bit puzzled as to why TLC hangs, I feel like it should be able detect that it "exhausted" the recursion but is still missing part of the mapping. Or that it is not making any progress, and error out?

Op maandag 22 juli 2024 om 23:19:02 UTC+2 schreef Hillel Wayne:

[Calvin Loncaric]

> I'm still a bit puzzled as to why TLC hangs

TLC does not memoize functions the way you might hope. A simpler example makes this behavior obvious:

---- MODULE Fib ----

EXTENDS Naturals

fib[n \in Nat] ==
    IF n \in {0, 1}
    THEN n
    ELSE fib[n-1] + fib[n-2]

\* This works fine.
ASSUME fib[1] = 1
ASSUME fib[2] = 1
ASSUME fib[3] = 2
ASSUME fib[4] = 3
ASSUME fib[5] = 5
ASSUME fib[6] = 8

\* ...But checking this assumption causes TLC to spin out!
\* Evaluating `fib[n]` takes exponential time.

\* Memoization of `fib` would make it very fast.
ASSUME fib[46] = 1836311903

Spec == TRUE /\ [][TRUE]_<<>>

====

This behavior is not fundamental. TLC could use an internal memotable for recursive functions like `fib` and `GoodBoard` to make them faster. It's not clear if that would be a good idea in general, since it might add memory or cpu overhead, but I think it might work great for recursive functions with finite domains (like `GoodBoard`).

--

Calvin

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1f987035-556e-4039-af46-1183bce5cfc9n%40googlegroups.com.