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

[Utkarsh Sharma <sharmautkarsh0504@xxxxxxxxx>]

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?

On Tuesday, February 18, 2025 at 7:16:11 AM UTC+11 Markus Kuppe wrote:

I didn’t review your spec, but the TLA+ Debugger [1] is likely a more reliable and effective tool for debugging your spec compared to using PrintT.

Markus

[1] https://www.youtube.com/watch?v=DsfbdsE4hJ0&list=PLWLcqZLzY8u9crK5PwTmEyBjgzHCotT60

> On Feb 17, 2025, at 1:50 AM, Utkarsh Sharma <sharmaut...@xxxxxxxxx> wrote:
>
> I'm trying to build operators that do floating point multiplication on Binary Numbers (which are represented as a sequence which match the IEEE754 floating point 32 bit specification). I'm defining Booth's algorithm recursively and then as a state machine (i.e. with a next transition and init). When i define it as a state machine I get the correct output but when I translate this across to a recursive function it gives me a different output to the state machine would. However, the strange part is, if I add PrintT statements within the recursion then I get the correct answer for the final state (but it returns with an error due to the predicate logic of PrintT /\ Recursion). Why is this happening? All I change is a printT statement added in there and suddenly i get the correct answer in the recursive case but without it, it gives me a wrong answer.
>
> As an example Ive attached a file below and some simple output case. When I add PrintT statements in the BoothLoop statement, we get the correct answer for the provided input but when I get rid of the PrintT statements, I get an incorect answer. The only thing I change is adding or not adding the PrintT statement in Line 53. (Example with red circle shows the correct answer but when I get rid of the PrintT it returns the wrong final answer).
>
> --
> 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 visit https://groups.google.com/d/msgid/tlaplus/5da8f6e5-04fd-4488-9e43-eeeb35a2cc7cn%40googlegroups.com.
> <image.png><image (1).png><FixedPointMult.tla>

-- 
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/2227e27b-03b2-40bc-86c2-cad5ce7ca93en%40googlegroups.com.

Attachment: Screenshot 2025-02-18 132353.png
Description: PNG image