TLA+ specifications

Here are some specifications written in TLA+ and a docker container for running the TLC model checker.

The repository layout is as follows:

.
├── container               -  Container definition for TLA+ tools
│   └── run.sh              -  Builds and runs the TLA+ container in interactive mode
└── src
    ├── video_exercises     -  Exercises based on Lamport's video lectures
    └── own_problems        -  My own (various) specifications.

Tools in the container

• tlc $SPEC runs the model checker on $SPEC.tla with the configuration in $SPEC.cfg
• tla2pdf $SPEC converts $SPEC.tla into a PDF document, $SPEC.pdf, via Latex
• animate_tlc_trace $SPEC converts the TLC trace output of a failing $SPEC.tla into an SVG-based animation in $SPEC.html
  • It expects the associated configuration $SPEC.cfg to define a VIEW where that VIEW maps each state onto an SVG group. See src/own_problems/StateTransferAnimated.tla for example.

Useful links

Videos

• Lamport's TLA+ video lectures
• Dr TLA+ series

Community

• Lamport's TLA+ website
• TLA+ google group
• TLA+ community-provided modules
• TLA+ examples

Configuration syntax

• TLC configuration file syntax

Tools/utilities

• TLA+ web-based behaviour explorer
• TLA+ behaviour animations