[tlaplus] Error(s) from running the Trace Explorer

["myzh...@xxxxxxxxx" <myzh1989@xxxxxxxxx>]

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

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/943c9489-e025-41e1-8573-e931f0fbf90an%40googlegroups.com.