The information the future can still ask for

Consider two job-service snapshots:

If the only possible next action were “show whether something is running,” the attempt numbers could be erased. Both snapshots answer identically. But admit a delayed Complete(7) action. Snapshot A may accept that completion; snapshot B must reject it as stale. The next observation differs.

This is the future-separation test:

State is not the event log

An event log may record Accepted(7), Started(7), Retried(8), and Started(8). The model does not automatically need all four events. It needs the summary that preserves later choices: active attempt 8, the set of attempts whose completion may still arrive if the environment admits that behavior, available capacity, and publication state.

History becomes state only when a future rule reads it. If the protocol rejects every repeated request identity forever, the set of applied request identities is state. If audit text cannot affect any modeled transition or observation, it is outside this model even if production retains it for years.

This distinction reduces a common modeling failure: copying a database schema into a checker. Storage fields are evidence about what the implementation remembers. They are not a proof that the model needs the same representation.

Build the carrier

For the publication question, one adequate state might be:

activeAttempt  one attempt identity or none
phase          idle, running, canceled, completed
credit         0 or 1
published      one attempt identity or none

The carrier forbids some illegal combinations by construction. A single phase value cannot be both running and canceled. A single publication slot cannot contain two attempt identities. Other impossible combinations still need a property: credit = 0 while phase = idle may reveal a leaked credit.

Experienced engineers should separate semantic state from physical layout. The mathematical carrier above might become an enum and two optional values, a packed integer, a record, or relations in a specification language. Those representations may have different performance. They must preserve the same admitted states and observations before a representation comparison is meaningful.

Under the hood: an equivalence relative to observation

Let a concrete implementation situation be $c$, and let an abstraction function map it to model state $a(c)$. The model deliberately treats $c_1$ and $c_2$ as equivalent when

$$a(c_1) = a(c_2).$$

That equality is justified only relative to the admitted action sequences and observations. For every such future sequence, either both concrete situations admit it with the same relevant observation, or neither does. The chapter does not require proving a full refinement relation yet. It gives the adversarial question that discovers missing state early: “What future could tell these two apart?”

State minimization is therefore not aesthetic tidying. Removing a value is a claim that the value cannot influence any modeled future observation. Adding a value is a claim that some admitted future needs the distinction. Both claims can be challenged with a witness.

When more state is the repair

Engineers often hear “keep state small” and delete identity, provenance, or generation information. That can make a model smaller by making the intended property inexpressible. Small is not the goal. Adequate is the goal; smallness follows only after adequacy.

For the job service, attempt identity repairs the abstraction. Later, tool chapters will show a different repair: moving nondeterministic network contents into state so a checker, rather than the host runtime, owns delivery order.

Lessons

• State is the information required to determine every admitted later observation.
• Two situations that look the same now may need different states when a future action separates them.
• An event log is history; only future-read history belongs in this model's state.
• Mathematical state and physical storage layout are separate design choices.
• “Small state” is subordinate to adequate state.

Practice

1. Retrieval. State the future-separation test in one sentence.
2. Discrimination. A queue model records item order but not the timestamp at which each item arrived. When is that omission sound?
3. Transfer. A password-reset link may be used once. Name the smallest state needed to distinguish an unused link, a used link, and a newly issued link that happens to target the same account.

References

1. Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — states, behaviors, specifications, and abstraction in TLA+
2. Christel Baier and Joost-Pieter Katoen. “Principles of Model Checking.” MIT Press, 2008. — transition systems, state equivalences, and temporal properties