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.
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.