• 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.

• 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: Class's methods are assumed to be thread-safe.

• MemFPSet
  • MemFPSet1 (marked as deprecated)
  • MemFPSet2
• NoopFPSet
• MultiFPSet
• DiskFPSet: abstract class. Uses a bounded amount of memory. Any fingerprints that don't fit in memory are written to backing disk files.
  • NonCheckpointableDiskFPSet
    • OffHeapDiskFPSet
  • HeapBasedDiskFPSet
    • LSBDiskFPSet
      • DummyDiskFPSet
    • MSBDiskFPSet
      • DummyFPSet in TLCServerTestCase
  • MemFPSet
  • FaultyFPSet

Pratically speaking,

TLCState is implemented by a tons of different classes for some 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.