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

Error Trace Exploration

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?