TLA⁺

• Homepage
  • video
  • learning
  • Specifying Systems: book
• PlusCal
• Learn TLA+
• google group: tlaplus
• github
  • tlaplus: releases
  • examples
• LaTeX

---

Install Toolbox

• tlaplus/tlaplus: releases
• LaTeX
  • MacTeX

which pdflatex

/Library/TeX/texbin/pdflatex

Usage

1. File → Preferences
   • Specifiy pdflatex command: /Library/TeX/texbin/pdflatex
2. File → Open Spec → Add New Spec...
   • Root-module file: SimpleProgram.tla
   • Specification name: SimpleProgram
3. File → Produce PDF Version: Option + Command + P

Check TLC Model Checker

TLC Model Checker → New Model... → ▶︎ Runs TLC on the model.

Model Overview → Uncheck: Deadlock → ▶︎ Runs TLC on the model.

Help

1. Help → Table of Contents
2. Read: Getting Started