Re: [tlaplus] Recursion without StackOverflowError

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

M.

> On Jul 22, 2024, at 2:22 PM, Isaac Dynamo <isaacdynamo@xxxxxxxxx> wrote:
> 
> 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:
> 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 
> 
> 
> On 7/19/24 10:29 AM, 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, 
> 
> -- 
> 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/e890b810-5fcf-482b-8c9b-0316bddded91n%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/F822781F-FE33-4893-960A-FC233AB54571%40lemmster.de.