[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!


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.