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

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Thomas,

I cannot answer your question about 32-bit integers in TLC. It
probably has to do with java.lang.Integer.

I am just curious about your experiments with the Collatz conjecture.
Are you trying to do a random simulation of the Collatz conjecture
with TLC? I can imagine that TLC would be able to do breadth-first
search on a relatively small input space.

You could check the Collatz conjecture with Apalache for a bounded
number of steps, as it supports unbounded integers out of the box.
Below is the TLA+ generated by ChatGPT. I just added the type
annotation for x. Here is how I would check the conjecture for all
executions up to 15 steps:

```
apalache-mc check --temporal=CollatzConjectureSimple --length=20 Collatz.tla
```

Apalache does not find any counterexamples to <>(x = 1), as it uses
the definitions of Init and Next and ignores stuttering by default.
After 15 steps it slows down significantly, as the SMT solver (z3)
seems to hit the limits of solving integer constraints of larger
dimensions.

---------------------------- MODULE Collatz ----------------------------
EXTENDS Naturals

VARIABLE
    \* @type: Int;
    x

CollatzStep(n) == IF n % 2 = 0 THEN n \div 2 ELSE 3*n + 1

Init == x \in Nat \ {0}

Next == x' = CollatzStep(x)

Spec == Init /\ [][Next]_x

CollatzConjectureSimple == <>(x = 1)
CollatzConjecture == <>[](x \in {1,2,4})
=============================================================================

Best regards,
Igor

On Mon, Jul 28, 2025 at 7:08 PM 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.

-- 
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/CACooHMDCRjXOe3ada%2BuuMVD-qKwhkpw%2BgAR9znwFaX%3DaARRJLA%40mail.gmail.com.