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

*From*: Isaac Dynamo <isaacdynamo@xxxxxxxxx>*Date*: Fri, 19 Jul 2024 10:29:08 -0700 (PDT)

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)

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

-- 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.

**Follow-Ups**:**Re: [tlaplus] Recursion without StackOverflowError***From:*Hillel Wayne

**Re: [tlaplus] Recursion without StackOverflowError***From:*Markus Kuppe

- Prev by Date:
**[tlaplus] Re: TLA+ Foundation Grants** - Next by Date:
**[tlaplus] Re: TLA+ Foundation Grants** - Previous by thread:
**[tlaplus] Re: TLA+ Foundation Grants** - Next by thread:
**Re: [tlaplus] Recursion without StackOverflowError** - Index(es):