Write a script that determines whether an actual execution trace (extracted from the logs after a replica set test) matches a trace permitted by a given TLA+ spec. The exact technique is TBD; it will involve some interaction between TLC and our custom checking code.

Questions:

• Dump the whole state graph and check the trace with Python (Jesse's Skunkworks script) or follow Pressler's "Verifying Software Traces Against a Formal Specification with TLA+ and TLC"?
• Use/disable TLC's "symmetry set" optimization?
• In addition to checking that we go from one permitted state to another, also check that we get there only by executing actions enabled in the spec?