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