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 19:57] – 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. +
- +
-===== 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 (deprecated) +
-  * 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. +
  • user/fponzi.1731527824.txt.gz
  • Last modified: 2024/11/13 19:57
  • by fponzi