Repository files navigation

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.

• 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 aVIEW where thatVIEW maps each state onto an SVG group. Seesrc/own_problems/StateTransferAnimated.tla for example.

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

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

• TLC configuration file syntax

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