TLA⁺ Examples

This is a repository of TLA⁺ specifications and models covering applications in a variety of fields. It serves as:

• a comprehensive example library demonstrating how to specify an algorithm in TLA⁺
• a diverse corpus facilitating development & testing of TLA⁺ language tools
• a collection of case studies in the application of formal specification in TLA⁺

All TLA⁺ specs can be found in the specifications directory. A central manifest of specs with descriptions and accounts of their various models and features can be found in the manifest.json file.

List of Examples

License

The repository is under the MIT license. However, we can upload your benchmarks under your license.

Support or Contact

Do you have any questions or comments? Please open an issue or send an email to the TLA+ group.

Contributing

Do you have your own case study or TLA⁺ specification you'd like to share with the community? Follow these instructions:

1. Ensure your spec is released under MIT or a similarly-permissive license
2. Fork this repository and create a new directory under specifications with the name of your spec
3. Place all TLA⁺ files in the directory, along with their .cfg model files; you are encouraged to include at least one model that completes execution in less than 10 seconds
4. Ensure name of each .cfg file matches the .tla file it models, or has its name as a prefix; for example SpecName.tla can have the models SpecName.cfg and SpecNameLiveness.cfg, etc.
5. Consider including a README.md in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself
6. Add an entry to the below table in this top-level README.md summarizing your spec and its attributes

Adding Spec to Continuous Integration

To combat bitrot, it is important to add your spec and model to the continuous integration system. To do this, you'll have to update the manifest.json file with machine-readable records of your spec files. If this process doesn't work for you, you can alternatively modify the .ciignore file to exclude your spec from validation. Otherwise, follow these directions:

1. Ensure you have Python 3.11+ installed
2. Download & extract tree-sitter-tlaplus (zip, tar.gz) to the root of the repository; ensure the extracted folder is named tree-sitter-tlaplus
3. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path
   • On Windows, this might entail running the below script from the visual studio developer command prompt
4. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run python -m venv . then source ./bin/activate on Linux & macOS or .\Scripts\activate.bat on Windows (run deactivate to exit)
5. Run pip install -r .github/scripts/requirements.txt
6. Run python .github/scripts/generate_manifest.py
7. Locate your spec's entry in the manifest.json file and ensure the following fields are filled out:
   • Spec title: an appropriate title for your specification
   • Spec description: a short description of your specification
   • Spec source: if this spec was first published elsewhere, provide a link to this location
   • Spec authors: a list of people who authored the spec
   • Spec tags:
     • "beginner" if your spec is appropriate for TLA⁺ newcomers
   • Model runtime: approximate model runtime on an ordinary workstation, in "HH:MM:SS" format
   • Model size:
     • "small" if the model can be executed in less than 10 seconds
     • "medium" if the model can be executed in less than five minutes
     • "large" if the model takes more than five minutes to execute
   • Model mode:
     • "exhaustive search" by default
     • {"simulate": {"traceCount": N}} for a simulation model
     • "generate" for model trace generation
   • Model config:
     • "ignore deadlock" if your model should ignore deadlock
   • Model result:
     • "success" if the model completes successfully
     • "safety failure" if the model violates an invariant
     • "liveness failure" if the model fails to satisfy a liveness property
     • "deadlock failure" if the model encounters deadlock
   • Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the manifest-schema.json file)

Before submitted your changes to run in the CI, you can quickly check your manifest.json for errors and also check it against manifest-schema.json at https://www.jsonschemavalidator.net/.