TLC Nat and Integers...still using 32 bit?

[thomas...@gmail.com]

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. 

[Igor Konnov]

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

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

[Andrew Helwer]

Regarding 32- or 64- bit arithmetic, TLC already does not work on 32-bit architectures due to a 64-bit atomic compare-and-swap operation it does on the fingerprint set, which uses 64-bit hashes. So theoretically there shouldn’t be any performance hit to using longs for arithmetic instead of ints. It is possible it would cause the pending state set to take up more memory, though. I don’t know whether 32-bit integers are already aligned to a 64-bit boundary in Java datastructures, or what.

BigInteger isn’t a good idea in my opinion because TLC models tend to use small numbers amidst combinatoric state explosion, so performance is very important.

Andrew Helwer

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CACooHMDCRjXOe3ada%2BuuMVD-qKwhkpw%2BgAR9znwFaX%3DaARRJLA%40mail.gmail.com.

[Markus Kuppe]

Generally, it's best to discuss TLC bugs and enhancement requests at github.com/tlaplus/tlaplus. That said:

TLC does work on 32-bit architectures. However, in that environment, you won’t be able to take advantage of the faster CAS-based fingerprint set implementation and will have to rely on the slower, platform-independent version instead.

As for switching TLC from 32-bit to 64-bit integers: I don’t see how this could be done without significant cost. At a minimum, it would double the on-disk representation of integers, unnecessarily increasing storage usage in most cases. This doesn't even account for the potential for subtle bugs introduced by changing from int to long. Java’s type system doesn’t make such transitions trivial in a complex codebase like TLC’s.

More fundamentally, I’d want to see a broader set of real-world specs and models that would benefit from 64-bit integers. For most existing TLC models, this change would result in slower performance with no practical gain. We would essentially be optimizing for an outlier. As Igor mentioned, these scenarios are better served by a tool like Apalache, which is designed for symbolic execution and unbounded arithmetic. TLAPS is another tool to mention here.

Markus

[Thomas Gebert]

I don't think "doubling the on-disk representation" of integers would be significant for most users, if any.  Disk space and memory is very cheap. Additionally, the values have wrapper types anyway:  https://github.com/tlaplus/tlaplus/blob/6479e53ae1e418a1bfe31677ad45012fe8ed7008/tlatools/org.lamport.tlatools/src/tlc2/value/impl/IntValue.java#L19 .  This means (I think) that the value will be heap-allocated, and as such will have a 64 bit pointer attached to it for reference and deference.  As such, I don't think the difference from "int" to "long" would be significant.  

I'm skeptical of the claim that it would result in "slower performance".  64 bit CPUs should be able to handle longs at the same speed as ints, and I suspect that whatever performance "gains" you would get from using 32 bit int would be dwarfed several times over by the latency of fetching from the heap to unbox the value. 

My goal was actually to use TLAPS, and I was just using TLC to sanity check my implementation of Collatz, because obviously a model checker can't check the entirety of naturals, though I think TLAPS doesn't have support for some of the operators I'd need for my ideas. 

[Andrew Helwer]

With respect to memory at least, reducing its use is very desirable. Ideally the entire pending state set can be kept in memory, and performance degrades nonlinearly if not. However, all of this is speculation and would be well served by actual measurement of the changes’ performance impact.

Andrew

--
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/3578a141-6759-41e9-b45b-5b03d64ca517n%40googlegroups.com.

[Irwansyah Irwansyah]

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

--

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

[Michael Leuschel]

Hi,

for your information, the ProB tool can also handle some TLA+ specifications.
It works on the model generated by Igor. I have slightly adapted it to start with
a specific value (2^65) where it reaches the value 4 on the 64th step. See the screenshot below.

FYI: ProB uses Prolog's tagged 64 bit values (4 bits used for tagging to distinguish floats, integers, atoms, …),
leaving 60 bits to represent integers. It, transparently switches to unlimited big integers if needed.
The CLP(FD) finite domain solver is, however, limited to 60 bits, but can be turned off. For the simple example below it is not needed.

For explicit state model checking it is typically considerably slower than TLC, but it can also be considerably faster for high-level models which can profit from constraint solving (e.g., N-Queens). It also provides interactive animation, visualisation features which complement TLC. (It can also use TLC as an alternative backend for model checking low-level B models.) More details can be found here: https://prob.hhu.de/w/index.php?title=TLA.


Greetings,
Michael

> On 29 Jul 2025, at 10:14, Igor Konnov <igor....@gmail.com> wrote:
>
>
> 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:

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

VARIABLE
\* @type: Int;
x

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

Init == x= 36893488147419103232 \* 2^65, model checking time 3 ms, 66 states
\* x = 774840977 \/ x = 576460752303423488
\* x \in Nat \ {0}

Next == x' = CollatzStep(x)

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

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

\* some preferences for ProB (see https://prob.hhu.de/w/index.php?title=TLA)
\* they are not required for the example as it is above, but could be useful if you modify it
SET_PREF_MAXINT == 10000 \* only relevant for unbounded enumeration of Nat/Int
SET_PREF_MAX_INITIALISATIONS == 10001 \* controls number of Init solutions computed; increase
SET_PREF_CLPFD == TRUE \* you may have to set it to FALSE if x is initialised non-deterministically with possibly values >= 2^59
ASSERT_LTL == "F G {x=1 or x=2 or x=4}" \* LTL formula for ProB

=============================================================================