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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

> On Jul 29, 2025, at 7:49 AM, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
> 
> 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.

-- 
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/4A177DD2-B0F1-4C71-AC33-B7387CDF4E97%40lemmster.de.