Error(s) from running the Trace Explorer

[myzh...@gmail.com]

Dear all,

I am trying to visualize the error trace by following Issue #267: Self-referential error trace exploration: _TEPosition and _TETrace operators.

However when I put the following into the "Error-Trace Exploration" and start "Explore". 

"Host == LET n == _TEPosition

        IN IF n = 1 

           THEN "Init"

           ELSE LET this == _TETrace[n].pc

                    prev == _TETrace[n - 1].pc

                IN CHOOSE p \in DOMAIN prev : prev[p] # this[p]"

The toolbox throws the following error:

"Error(s) from running the Trace Explorer:

Java ran out of memory.  Running Java with a larger memory allocation

pool (heap) may fix this.  But it won't help if some state has an enormous

number of successor states, or if TLC must compute the value of a huge set."

On another machine, I have another error message which says that 

"An internal error occurred during: "Exploring the trace...".

GC overhead limit exceeded"

Based on my understanding of "Error-Trace Exploration", it just evaluates the new expression at each step in the error trace, so it should not have a big overhead, right?

I have attached the MC_TE.out and TE.tla. I do not quite understand the purpose of those generated files by the toolbox. Please let me know if more files are needed.

Thanks in advance!

Mingyang

[myzh...@gmail.com]

The attachment is too large (TE.tla, 2.1M and MC_TE.out 0.6M), which prevents me to share here. 

[Markus Kuppe]

On 27.04.21 23:49, myzh...@gmail.com wrote:
> The attachment is too large (TE.tla, 2.1M and MC_TE.out 0.6M), which
> prevents me to share here.

Hi Mingyang,

please send it to me privately or open an issue at
https://github.com/tlaplus/tlaplus/issues

Thanks,
Markus