Practical TLA+: Planning Driven Development

Appendix A: Math

Most of the math that TLA+ uses is relatively simple, but not everybody has the background, so this appendix is here to help you learn what you need to know to use TLA+. This is not intended to be a rigorous or complete introduction, just enough to give you some intuition for writing TLA+ operators. You can read a more in-depth treatment of this that’s still oriented toward TLA+ in the original Specifying Systems book, which is provided in the toolbox under Help > Specifying Systems .

Most math uses a different notation than most programs. In C, you have ! for “not”, && for “and”, and || for “or”. The corresponding math notations are ¬, ∨, and ∧, none of which are part of default keyboards. That’s why in TLA+ we use ~, /\, and ...