TLA+
Introduction
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.
Mathematics
| 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.
- Each wire must occur between two different people in the bank and wire at least one dollar;
- If the wire succeeds, value of the wire is deducted from the sender and added to the receiver;
- If the wire fails, the two accounts are unchanged;
- A wire may not cause an account to have a negative balance;
- Multiple wires my occur simultaneously.