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

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

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 <sharmautkarsh0504@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+unsubscribe@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/AAD68482-C674-4DC6-B6B0-EA40D0A8D098%40lemmster.de.