This is an old revision of the document!
Diving into tlatools
- 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.
Questions:
What is a Trace?
- 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.
How does MP works?
What’s the high level overview of the dependencies across classes?
What’s the goal for Tool class?
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.
FPSet
Represents a set of 64-bit fingerprints. FPSet is an abstract class. Default implementation is
Implementors:
- DiskFPSet.java
- DummyDiskFPSet.java
- HeapBasedDiskFPSet.java
- LSBDiskFPSet.java
- MemFPSet.java
- MemFPSet1.java
- MemFPSet2.java
- MSBDiskFPSet.java
- MultiFPSet.java
- NonCheckpointableDiskFPSet.java
- NoopFPSet.java
- OffHeapDiskFPSet.java
What is TLCState?
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.
What is TLCStateMut?
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.
fponzi