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

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



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.