35 lines
2 KiB
Markdown
35 lines
2 KiB
Markdown
# Best current practices for designing systems with TLA+
|
|
|
|
(According to Claude 3.5: Sonnet - 2025-02-20)
|
|
|
|
1. Start with High-Level Specifications:
|
|
- Begin by specifying the high-level properties and behaviors of the system.
|
|
- Focus on safety (nothing bad happens) and liveness (something good eventually happens) properties.
|
|
2. Use Simple and Clear Definitions:
|
|
- Keep your specifications simple and clear.
|
|
- Use meaningful names for variables and operators to improve readability.
|
|
3. Incremental Refinement:
|
|
- Develop your specification incrementally.
|
|
- Start with an abstract model and gradually refine it to add more details.
|
|
4. Leverage TLA+ Modules:
|
|
- Use existing TLA+ modules (e.g., Integers, Sequences) to avoid reinventing the wheel.
|
|
- Extend modules to reuse common definitions and operators.
|
|
5. Model Checking Early and Often:
|
|
- Use the TLC model checker to verify your specifications early in the development process.
|
|
- Regularly check for invariants and properties to catch errors early.
|
|
6. Document Assumptions and Invariants:
|
|
- Clearly document the assumptions and invariants in your specifications.
|
|
- Use comments to explain the purpose and logic of complex expressions.
|
|
7. Use PlusCal for Algorithmic Specifications:
|
|
- Use PlusCal for specifying algorithms in a more familiar, imperative style.
|
|
- Translate PlusCal code to TLA+ to leverage the power of TLA+ for verification.
|
|
8. Test with Different Configurations:
|
|
- Test your specifications with different initial states and parameters.
|
|
- Use TLC configuration files to manage different test scenarios.
|
|
9. Collaborate and Review:
|
|
- Collaborate with team members to review and improve the specifications.
|
|
- Use version control to manage changes and track the evolution of your specifications.
|
|
10. Iterate Based on Feedback:
|
|
11. Iterate on your specifications based on feedback from model checking and peer reviews.
|
|
12. Continuously refine and improve the specifications to better capture the system's behavior.
|
|
|