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 Latexanimate_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.
- It expects the associated configuration