Differences

This shows you the differences between two versions of the page.

--- user:fponzi:diving [2024/11/13 20:37] – fponzi
+++ user:fponzi:diving [2024/12/17 00:59] (current) – removed fponzi
@@ Line 1: / Line 1: @@
-====== 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.
-====== 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.
-===== 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.
-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,
-===== What is TLCState? =====
-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.
-==== 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.