TLA+ gives different outputs based on a printT statement or not - Booth's Algorithm

[Utkarsh Sharma]

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).

[Markus Kuppe]

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...@gmail.com> 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...@googlegroups.com.
> 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>

[Utkarsh Sharma]

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?

[Markus Kuppe]

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

[Calvin Loncaric]

Hi,

I took a close look at FixedPointMult.tla, and it looks like you have indeed discovered a bug in TLC's evaluator! I've filed a GitHub issue:

https://github.com/tlaplus/tlaplus/issues/1145

And I am working on a patch.

In the meantime, you should be able to work around the bug by changing line 14 to

          newAns   == TLCEval([ans EXCEPT ![i] = sum % 2])

which changes TLC's evaluation algorithm slightly to take a bug-free path. (Normally TLCEval is a performance hint and should have no real effect, but in this case it forces an early evaluation that works around the bug.)

Thanks for the report!

Calvin

On Sun, Feb 16, 2025 at 4:50 PM Utkarsh Sharma <sharmaut...@gmail.com> 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).

--