user:fponzi

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
user:fponzi [2024/11/13 20:27] – fponziuser:fponzi [2025/07/04 09:00] (current) – created fponzi
Line 1: Line 1:
-====== Diving into tlatools ====== +Welcome to my page on the wiki!
- +
-  * 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. +
- +
-===== 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 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. +
  • user/fponzi.1731529639.txt.gz
  • Last modified: 2024/11/13 20:27
  • by fponzi