Error(s) from running the Trace Explorer

16 views
Skip to first unread message

myzh...@gmail.com

unread,
Apr 28, 2021, 2:43:47 AMApr 28
to tlaplus
Dear all,


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

unread,
Apr 28, 2021, 2:49:29 AMApr 28
to tlaplus
The attachment is too large (TE.tla, 2.1M and MC_TE.out 0.6M), which prevents me to share here. 


Markus Kuppe

unread,
Apr 28, 2021, 10:20:34 AMApr 28
to tla...@googlegroups.com

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
Reply all
Reply to author
Forward
0 new messages