1. Introduction
    1. Mathematics
  2. Chapter 1


This post contains notes from learning TLA+, a formal specification language for designing, modelling, documenting, and verifying concurrent systems.
These notes created from Practical TLA+, a book targeted towards TLA+ beginners.

TLA+ is an acronym for Temporal Logic of Actions.


Human Semantics TLA+ Math
not ~ $\neg$
and /\ $\wedge$
or \/ $\vee$
in \in $\in$
notin \notin $\notin$
True T $1$
False F $0$

Chapter 1

Use TLA+ to specify a bank wire transfer problem.

  1. Each wire must occur between two different people in the bank and wire at least one dollar;
  2. If the wire succeeds, value of the wire is deducted from the sender and added to the receiver;
  3. If the wire fails, the two accounts are unchanged;
  4. A wire may not cause an account to have a negative balance;
  5. Multiple wires my occur simultaneously.