Differences

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

--- user:fponzi [2024/11/13 19:49] – created fponzi
+++ user: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.
-===== 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 =====
-a set of 64-bit fingerprints.
-===== 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.