[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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
=============================================================================

--
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/8100723b-6297-4c54-8b13-e4f3b81ff8a4n%40googlegroups.com.

Attachment: DecimalConverter.tla
Description: Binary data

Attachment: DecimalDivider.tla
Description: Binary data

Attachment: DecimalExponentiation.tla
Description: Binary data

Attachment: DecimalMultiplier.tla
Description: Binary data

Attachment: DecimalAdder.tla
Description: Binary data