[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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

--
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/CABf5HMhu%3Dhr8169%2BXp-UqunbU5fhLYDKP65SLPX2EzZm3v8mKA%40mail.gmail.com.