[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Recursion without StackOverflowError



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

On 7/19/2024 12:29 PM, Isaac Dynamo wrote:
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)

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




--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5edb0bb5-a335-4518-88a3-dee7fb9b9d05n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba63dca-b8d1-4244-ad22-7e59393ae185%40gmail.com.