First I want to thank all of you for your help. I finally begin get a little grip of TLA+ and I love it! It's simply fantastic! The error trace is like an omniscient debugger, a programmer's dream come true.
I was wondering is there a way to save and later load or even share the error-trace? The interesting ones often takes hours to produce, and the trace is very valuable for a group discussion about what went wrong and how should it be fixed. Or can a set of explored states be preserved and another set of predicates be evaluated against them?
And for the simulation mode, can I point to a state in an error-trace and tell the model checker to start from that particular state and begin exploring? Or can I point to a state and find out all the possible next step could be?
Thanks!