Reading a model¶
A formal model makes a rule precise enough to ask whether a proposed change is allowed. Start with a small payment: a participant has five tokens and wants to spend two. The useful questions are what the model records, which changes it permits, and which claims have actually been checked.
This reading path assumes no earlier TLA+ knowledge. The examples use a two-seat system in which the seats can have different permissions. A small example about one participant’s tokens does not define the other participant’s permissions or the whole game.
Begin with the state¶
A state is the collection of values recorded at one instant. In the payment example, available records spendable tokens. Other fields record whether a payment has occurred and whether its completion work is still pending.
Read a state table before reading a formula:
Question |
Before a payment |
After spending two |
|---|---|---|
How many tokens are available? |
Five |
Three |
Has payment occurred? |
No |
Yes |
Is completion work pending? |
No |
Yes |
This table explains the intended change. It is an authored example, not a captured model-checker trace. The released definition and its evidence determine which exact model supports it.
Read a transition as a relation¶
An action describes allowed pairs of states: one before the action and one after it. TLA+ writes an unprimed variable for its value before the action and a primed variable for its value after it.
available' = available - 2
Read this as “the next value of available equals its current value minus two.” The equality constrains two values; it is not an instruction that runs before the next line.
An action usually combines conditions:
/\ available >= 2
/\ available' = available - 2
The /\ symbol means and. Both conditions must hold for the proposed step. A state with one available token cannot take this action. The false guard supplies no permitted payment step; an implementation that accepts requests must separately preserve its state when rejecting one.
Look for what stays unchanged¶
A payment should not silently change an unrelated score. The model needs to constrain that field too:
UNCHANGED score
Read this as score' = score. Such constraints are called frame conditions. A field omitted from an action’s constraints is not automatically preserved. When reading a larger action, find both its intended changes and the frame around those changes.
Separate a start, a next step and a lasting claim¶
Init describes permitted starting states. Next describes permitted steps. An invariant is a condition that should hold in every reachable state. For example:
available >= 0
This invariant rules out a negative balance. It does not explain how payment works, show that payment eventually finishes, or establish that every possible cost is payable. Those are different questions.
The values and state chapter develops the notation. The checking chapter explains what a finite result can establish. Then follow resources and payment from an example to its exact definitions.
Follow an explanation to its evidence¶
Use Learn to build a mechanism from its assumptions. Use Reference to look up a definition without repeating the whole lesson. Use Evidence to inspect the particular model, configuration, properties and outcome behind a claim.
Check the release context when following a deep link or opening a saved source bundle. An explanation, definition and result must describe the same inputs before they can support one another. A successful page render is not a model-checking result.
Before continuing, try describing the five-to-three payment in your own words. Identify its precondition, changed values and an unrelated field that must stay unchanged. You should be able to do that before interpreting the entire formula.