• TLC.java
• public int process() is like the main method

Model checker.java extends AbstractChecker

does initialization, create initial state space, if there is next actions will call runTLC from AbstractChecker.

src/tlc2/tool/TLCStateFun.java: can be easily removed seems unused anywhere.

• Stores the sequence of states explored during model checking in a file with the extension .st.
• Provides methods to manage and access this trace information.

This class provides useful methods for tools like model checker and simulator. It’s instance serves as a spec handle

This is one of two places in TLC, where not all messages are retrieved from the message printer, but constructed just here in the code.

Tool → FastTool → Spec → SpecProcessor→ Sany.

Represents a set of 64-bit fingerprints. FPSet is an abstract class. Type hierarchy: FPSet

* MemFPSet

• MemFPSet1 (marked as deprecated)
• MemFPSet2

* NoopFPSet * MultiFPSet * DiskFPSet

• NonCheckpointableDiskFPSet
  • OffHeapDiskFPSet
• HeapBasedDiskFPSet
  • LSBDiskFPSet
    • DummyDiskFPSet
  • MSBDiskFPSet
    • DummyFPSet in TLCServerTestCase
• MemFPSet
• FaultyFPSet

TLCState is implemented by a tons of different classes for unknown reason. They were refactored at some point, so just a bunch of classes that extend it still exist: TLCStateMut, TLCStateFun (used for custom operator I think?), TLCStateMutExt, TLCStateInfo, TLCStateVec.

represents a TLA+ state, which simply is an assignment of explicit values to all the global variables. This is the mutable version, which means that in-place updates are used for improved performance and reduced allocation. Compared to TLCStateMut, TLCStateMutExt remembers its predecessor (or null if initial state), the action that created it, and a Callable.