Re: [tlaplus] TLC Nat and Integers...still using 32 bit?

Hi Thomas,

Integers module extends Naturals. I believe this is the code for Naturals: https://github.com/tlaplus/tlaplus/blob/6479e53ae1e418a1bfe31677ad45012fe8ed7008/tlatools/org.lamport.tlatools/src/tlc2/module/Naturals.java#L61

Naturals is using int which is always 32-bits in Java. But Java's integer maxsize is 2147483647 which is still a lot bigger than 774840977. So why it caused overflow on your end?

Irwan

On Tue, Jul 29, 2025 at 12:08 AM thomas...@xxxxxxxxx <thomasgebert@xxxxxxxxx> wrote:

I decided to waste my time modeling the Collatz Conjecture, and I was shocked to see that 774840977 caused an overflow.

Unless I'm mistaken, TLC is still using a 32 bit integer?

In 2025 is there any reason not to use use a long instead of an int? I'd be happy to make a PR converting it to long if people think there would be value in that.

Personally I think that BigInteger fits more into the ethos of what TLA+ is supposed to be (an abstract model, not a programming language), but I realize that that would carry a performance overhead that might upset many people.

--
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/4b253500-3a60-4b85-9bbe-a62e1fff4f56n%40googlegroups.com.