Error Trace Exploration

[Chen Fu]

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!

[Markus Alexander Kuppe]

Hi Chen,

you can share the specification folder including its model
subdirectory¹. When the spec is added to another Toolbox, the error
trace will show up again automatically when the model editor opens. You
can also use error trace exploration.

TLC does not store states. It stores state fingerprints for efficiency
reasons instead. Thus, if you want to check new predicates, you will
have to start TLC with the new predicates. If model checking takes
hours, distributed TLC might be for you [1] (unless you need liveness
checking).

For simulation to start from a particular state, you will have to
manually specify the Initial predicate in your spec accordingly. Then
just run regular simulation from the model editor.

¹ The "Properties" dialog - accessible from the "Spec Explorer"'s
context menu - reveals the spec's on-disk location.

Cheers
Markus

--

[1]
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/distributed-mode.html

[Chen Fu]

Thanks Markus.

I will look into distributed mode. Currently I am doing safety check only, but I will need liveness check eventually :-)