Re: [tlaplus] TLA+ gives different outputs based on a printT statement or not - Booth's Algorithm

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

Please provide the specifications and model where the debugger encounters this issue.

The debugger displays a value for k at each level of recursion.  You can determine which value corresponds to which level by manually navigating to an earlier stack frame in the call stack.

Markus

> On Feb 18, 2025, at 3:47 AM, Utkarsh Sharma <sharmautkarsh0504@xxxxxxxxx> wrote:
> 
> I created another spec that is somewhat similar and uses a Recursion. For some reason my context and constants get stuck in the debugger for some reason and I can't step over or into anything else when this happens. It always happens in the second time that the loop of the MultRec operator happens and it gets and populates the correct answer for newAns in the first loop. The final returned answer is always the one that is given from k = 8 (i..e the first loop of the recursion, which is incorrect). I also have two values for k in my debug context. Is this normal and do you have any suggestions for why this behaviour is happening?


-- 
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 visit https://groups.google.com/d/msgid/tlaplus/5FC85463-91ED-4CA3-AEE3-E87192580266%40lemmster.de.