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

[Michael Leuschel <michael.leuschel@xxxxxxxxx>]

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.konnov@xxxxxxxxx> 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

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

-- 
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/4933B284-95E2-4012-A3FF-EECFFF5A85BB%40gmail.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/4933B284-95E2-4012-A3FF-EECFFF5A85BB%40gmail.com.