[tlaplus] Trace explorer overload?

["J.D. Meadows" <tr1pl3.d3v@xxxxxxxxx>]

I've done a heck of a simulation run with a large input set (500 nodes). To ensure it stops at exactly one behavior I've artificially added an invariant that checks that never all processes are "Done". Otherwise the simulation keeps running (except in case of small n input values, when it stops alone for some reason unknown to me). This trick works and TLC throws an error when the system terminates. The 'Checking mode' form is configured to max 1 trace and max trace length of 1M (I have no idea if this will be enough, but the field is mandatory, so I've put a large value). Profiling is off.

Now the problem is how to inspect the last state. There has to be a terminal state somewhere since the invariant has been violated, and I know it is correct from other runs. But I can't see the terminal state anywhere. The Toolbox trace explorer doesn't show all the states, it stopped at state 191, which upon inspection is not the terminal one. The simulation has generated almost 500 MB of logs, in the form of 4 files (two MC.out files and two MC_TE.out files) in two respective model folders (one is the main, the other has some numbers in the name). I opened them with a text editor and the last state in the files is still not the terminal one, and it looks like the 191th state, so I guess that is what the GUI is showing. 

So I have a couple of questions:

1. Is there any way of recovering the complete trace from any other file?
2. In case I have to run it again, is there any way of preventing the overload and somehow view just the terminal state that caused the error?
   

-- 
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/aeed0cfa-278b-4f38-88b1-1e93dabb82d3n%40googlegroups.com.