Skip to content

ZachBray/tlaplus-specs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

21 Commits
 
 
 
 
 
 
 
 

Repository files navigation

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

Community

Configuration syntax

Tools/utilities

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published