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