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

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

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

> On Feb 25, 2025, at 9:38 PM, Utkarsh Sharma <sharmautkarsh0504@xxxxxxxxx> wrote:
> 
> \* 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

-- 
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/A3304E16-0C4C-449C-BC8C-F596D995F7A1%40lemmster.de.