On Wednesday, February 26, 2025 at 2:59:34 AM UTC+11 Markus Kuppe wrote:
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
> On Feb 23, 2025, at 8:35 PM, Utkarsh Sharma <sharmaut...@xxxxxxxxx> wrote:
>
> 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
> =============================================================================