I get a "Cannot invoke "tlc2.debug.TLCStackFrame.getTool()" because "f" is null"

[Utkarsh Sharma]

Apologies but this spec and its dependencies are very involved. I just want to note that each of the operators defined in each of the files below work (at least I'm pretty sure)

The spec I am evaluating is shown below and this has some link to the print EXCEPT issue maybe(?). Essentially, when I run this spec without debugging mode I get that:
"This was a Java StackOverflowError. It was probably the result

of an incorrect recursive function definition that caused TLC to enter an infinite loop when trying to compute the function or its application to an element in its putative domain." but the call stack was empty."

When I run the same error in debug mode, I now get:
"TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.NullPointerException

: Cannot invoke "tlc2.debug.TLCStackFrame.getTool()" because "f" is null"

The operators which I  have defined here work if I just evaluate the expressions by itself. And sometimes if I run the same spec again, it will randomly work and the invariant will be triggered (this is very rare). I'm not sure why the behaviour is happening and why I'm running into these errors since the individual operators work in isolation?

------------------------------- MODULE Roots -------------------------------

EXTENDS DecimalMultiplier, DecimalExponentiation, DecimalDivider

half == DecimalRepresentation(5, 0, -1)

ITERS == 5

InitialEstimate(S) == LET power == ToInt(SubSeq(S, 2, 4)) - 499 IN

                        IF power < 0 THEN DecimalRepresentation(1, 0, 0)

                        ELSE LET NormalisedExp == BuildList(power \div 2 + 499)

                               builded == <<S[1]>> \o Zeros(3 - Len(NormalisedExp))

                                \o NormalisedExp \o SubSeq(S, 5, 22)

                        IN DivideR(2, 0, 0, builded)

CONSTANT num_before, num_after, num_exp

VARIABLE S, xn, DD, i  

Init ==

  /\ S  = DecimalRepresentation(num_before, num_after, num_exp)

  /\ xn = half    

  /\ DD = DecimalRepresentation(0, 0, 0)

  /\ i  = 0

Next ==

  IF i >= ITERS THEN

    UNCHANGED << S, xn, DD, i >>

  ELSE IF i = 0 THEN

    /\ xn' = InitialEstimate(S)

    /\ i'  = i + 1

    /\ UNCHANGED << S, DD >>

  ELSE

    LET newDD ==  DivideB(S, xn)

        additive == DecimalAdd(xn, DD)

        new_xn   == MultiplyDecimalRep(half, additive)

    IN

      /\ DD' = DivideB(S, xn)

      /\ xn' = new_xn

      /\ i'  = i + 1

      /\ UNCHANGED << S, DD >>

invariant == i < ITERS

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

[Markus Kuppe]

What values of num_before, num_after, and num_exp are you using when you encounter these errors? I tested a few values, and in those cases, TLC did not throw a StackOverflowError but rightfully complained about DD being changed despite being declared as unchanged.

Markus

[Utkarsh Sharma]

Yep the DD being in the UNCHANGED is a mistake my apologies, but I was using num_before = 4, num_after = 0,  num_exp=10

[Utkarsh Sharma]

\* SPECIFICATION

\* Uncomment the previous line and provide the specification name if it's declared

\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.

CONSTANTS

     num_before = 4

     num_after = 0

     num_exp = 10

INIT Init

NEXT Next

\* PROPERTY

\* Uncomment the previous line and add property names

INVARIANT invariant

\* Uncomment the previous line and add invariant names

This was my .cfg file

[Markus Kuppe]

Your specification makes heavy use of recursive operators, which cause TLC to require a large stack during evaluation. As a result, TLC is running out of stack space while processing the spec. This issue is more likely to occur when the TLA+ debugger is enabled, as it consumes additional stack space.

To address this, you can increase the Java Virtual Machine stack size by adding the -Xss16m option when launching TLC. This option allocates a larger stack (in this case, 16 megabytes) for each thread, which helps prevent stack overflow errors.

For more details on the -Xss option, refer to https://docs.oracle.com/en/java/javase/21/docs/specs/man/java.html.

Markus