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

[Utkarsh Sharma <sharmautkarsh0504@xxxxxxxxx>]

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.

Attachment: image.png
Description: PNG image

Attachment: image (1).png
Description: PNG image

Attachment: FixedPointMult.tla
Description: Binary data