Glossary¶
Term Guide¶
- Action¶
A predicate that describes how a state “evolves”. Any boolean expression with a primed operator (like
x' = x). Actions are true if they describe the next state and false if they don’t. Multiple actions can be true at once, for example if two things happen in parallel.- Behavior¶
A sequence of states, or “timeline”, in the system.
- Enabled¶
An action is “enabled” if it can “happen” this step, ie potentially describe the next step.
- Fairness¶
A guarantee that a system will eventually “make progress”. Weak fairness says that if the given action is permanently enabled, it will eventually happen. Strong fairness says that if the action is not permanently disabled, it will eventually happen.
- Formal Methods¶
The discipline of writing rigorous, verified code.
- Formal Specification Language¶
A language you use to describe a system you’re building, so you can find errors in it.
- Function¶
A mathematical function, with a fixed domain. Programming functions are called operators.
- Invariant¶
Something that must be true at every state in the system. All invariants are safety properties.
- Liveness¶
A property that a good thing is guaranteed to happen. All liveness properties are temporal properties.
- Model¶
In TLA+, a specification + a set of injected parameters and required invariants.
- Model checking¶
The most common way of verifying a specification matches its properties: generate every possible behavior and exhaustively test if any of them break your properties. The model checker for TLA+ is called TLC.
- Operator¶
The TLA+ equivalent of a programming function. Operators with primed variables in them are called actions.
- PlusCal¶
A DSL for writing TLA+ algorithms.
- Predicate¶
A boolean expression.
- Property¶
Something we want to be true of the system. All properties in TLA+ can be broken into safety and liveness properties.
- Safety¶
A property that a bad thing doesn’t happen. Most (but not all) safety properties are invariants. All invariants are safety properties.
- Specification¶
- Spec¶
A rigorous mathematical description of the system you’re building.
- State space¶
The set of all possible states reachable by all possible behaviors in a model.
- Step¶
A single “tick” of the clock, changing some of the spec’s state. A behavior is composed of a sequence of steps.
- Stutter Step¶
A state transition that doesn’t change anything. All TLA+ specs are “stutter-invariant”, meaning they can always stutter between any two “real” actions. A behavior can stutter forever unless otherwise prevented by a fairness constraint.
- Temporal Property¶
A property that spans more than one state. For example, “the counter must never decrease” or
- Theorem Prover¶
An alternate way to formally verify specifications, where you mathematically prove it has the properties you want. Much more difficult than model checker and so this guide doesn’t cover it. The theorem prover for TLA+ is called TLAPS.
- TLA+¶
The “Temporal Logic of Actions”, used for modeling concurrent systems. A formal specification language. You can either write in TLA+ directly or use the PlusCal DSL.
- TLA+ Toolbox¶
The official TLA+ IDE.
- TLC¶
The name of the model checker for TLA+. The site uses “TLC” and “model checker” interchangeably.
State space explosion Quantifier Module Machine World