Hello everyone,
I am currently working on a TLA+ specification that is challenging to model-check with TLC for two main reasons:
- The state space is very large.
- The evaluation of properties (especially invariants) is computationally expensive.
To optimize my workflow, I would appreciate insights or references regarding the following questions about TLC:
1. Parallelism in TLC:
How does TLC handle parallelism, and how effective is it to use many cores? For instance, would running TLC with ~100 cores be beneficial, or are there diminishing returns due to synchronization overhead or other limitations?
2. Caching in TLC:
When and how does TLC cache information during model checking? Specifically:
- Does TLC cache results for constant operators only?
- Does it require that a (constant or non-constant) operator be called repeatedly with the exact same inputs to leverage caching?
3. Java Overloading for State-Dependent Operators:
I am aware that constant operators can be overloaded with Java code. However, is it possible to overload state-dependent operators or properties (e.g., invariants) by:
- Passing state variables as parameters to the operator, or
- Directly accessing state variables from within the Java code?
If any of these topics have been discussed before, I’d be grateful for pointers to relevant threads or documentation. Otherwise, I’d love to hear your experiences or suggestions!
Thank you in advance for your time and help.
Quentin