At its most basic, TLA+ is a written description of what a system is supposed to do. More specifically, TLA+ is a specification language for formally defining the behavioural properties of a system.
TLA+ is based on temporal logic, which is built on top of first-order logic and set theory, and provides some conveniences for working with large specifications for complex systems. You can think of a TLA+ specification as mostly ordinary math and logic, glued together with temporal logic for parts requiring it.
Most of TLA+ is actually a language for writing math, and for turning mathematical specifications into an engineering tool for designing complex systems. As such, to work effectively with TLA+ requires first understanding a bit of the math behind it. But don’t worry, none of it is that complex.
TLA+ uses logic at its base — propositional logic to be more precise. In
propositional logic, there are two base values
a handful of operators: ∧ (conjunction), ∨ (disjunction), ¬
(negation), ⇒ (implication), and ≡ (equivalence). These
operators should already be fairly familiar to most programmers but are
defined here, just in case:
∧ (conjunction) : F ∧ G equals
TRUE iff both F and G equal
∨ (disjunction) : F ∨ G equals
TRUE iff both F or G (or both) equal
- ¬ (negation)
- ¬F equals
TRUEiff F equals
- ⇒ (implication)
- F ⇒ G equals
TRUEiff F equals
FALSEor G equals
- ≡ (equivalence)
- F ≡ G equals
TRUEiff F and G both equal
TRUEor both equal
Implication (F ⇒ G) can be difficult to understand given the
definition alone. In more detail, it means F implies G, but why would
TRUE evaluate to
TRUE? By using some concrete numbers
we can arrange an expression like (n > 3) ⇒ (n 1), which, if n = 4,
will be TRUE ⇒ TRUE, which is a true statement. If n = 2, we get
TRUE, which is a true statement as well. And if n = 0, we
get FALSE ⇒ FALSE, which is also a true statement. In fact, the
only case where ⇒ evaluates to
FALSE is if you have a logically
FALSE statement, like
FALSE. As a truth table, we can
prescribe ⇒ as follows:
|F||G||F ⇒ G|
If you are ever in doubt about how to evaluate a statement in propositional logic, you can always write out truth tables for each element and evaluate them by hand.
Set theory is the foundation of regular math, and TLA+ leverages this foundation for writing specifications. Sets can have a finite or infinite number of elements, and each set is completely determined by the elements in the set — sets cannot contain duplicates. Sets contain a few operations of interest to TLA+:
- ∈ (set membership)
- x ∈ S is
TRUEif the element x is in the set S.
- ∩ (intersection)
- S ∩ T is the set of all elements in both S and T.
- ∪ (union)
- S ∪ T is the set of all elements in S or T (or both).
- ∖ (difference)
- S ∖ T is the set of all elements in S that are not in T.
- ⊆ (subset)
- S ⊆ T evaluates to
TRUEiff every element of S is an element of T.
Whereas propositional logic provides logical operators for individual elements, predicate logic provides operators for sets. Particularly:
- ∀ (universal quantification)
- ∀ implies that a statement holds for all elements in a set. It is usually read as “for all”.
- ∃ (existential quantification)
- ∃ implies that there exists an element in a set, for which a statement holds. It is usually read as “there exists”.
The formula ∀ x ∈ S : F asserts that formula F is TRUE for every element x in the set S. The formula ∃ x ∈ S : F asserts that formula F is TRUE for at least one element x in S.
And That’s All — For Now
These are the basics required to read and write TLA+. I will use these basics in future articles to show on TLA+.