Learn · All the Ways It Can Break

growing

One State Can Have Several Next States

Nondeterminism preserves choices so the checker—not the model author—must explore their consequences.

formal-methods, nondeterminism, transition-systems, concurrency, learn

You will replace a deterministic update function with a transition relation, construct the interleavings of two independent completions, and recognize three places where nondeterminism hides: scheduling, environment input, and failure. You will also learn when determinism is the correct model rather than a simplification error.

A function chooses; a relation admits

A deterministic update function has the shape “state and action produce one next state.” A transition relation asks a different question: which pairs of old and new states are allowed?

In words, write

current state  --admitted action-->  possible next state

The same current state may have several outgoing arrows. If both jobs A and B are ready, the action alphabet might admit Publish(A) and Publish(B). After one occurs, the other may still occur. The model has at least these two traces:

ready(A,B) → published(A) → published(A,B)
ready(A,B) → published(B) → published(A,B)

The final set is the same, but an intermediate observation may differ. If publication consumes the only credit, one ordering might expose a defect that the other does not.

Nondeterminism — the model admits more than one next state or behavior from the same current state. It describes unresolved choice; it is not a probability distribution. Learn more in Lamport's TLA+ overview.

Prediction — preserve the scheduler choice instead of making it in the fixture.

Three sources of choice

Concurrency is the obvious source, but not the only one.

Scheduling

Two enabled actions may occur in either order. Threads, actors, callbacks, and distributed nodes all create scheduling choices. A model need not reproduce a particular production scheduler. It must admit every order relevant to its claim unless a stated assumption rules one out.

Environment input

A user may cancel or wait. A message may contain any value in a declared finite domain. A clock reading may fall within an interval. The environment's choice becomes an action or an action parameter rather than a hidden call to a random number generator.

Failure

A message may arrive, be duplicated, be lost, or remain pending. A process may continue or crash. Modeling only the successful action makes reliability a premise rather than a conclusion.

These choices have no probabilities unless the model explicitly supplies a probability measure and uses a tool with the corresponding semantics. “Either may happen” and “each happens half the time” are different claims.

Under the hood: traces are paths through a graph

Take a set of states $S$ , a set of action labels $A$ , and a transition relation

$T \subseteq S \times A \times S.$

The sentence $(s,a,s') \in T$ means action $a$ may move state $s$ to state $s'$ . A finite trace is a path whose adjacent triples belong to $T$ . A checker does not invent behavior outside the relation. If the model omits message duplication, no amount of exhaustive search will discover a duplication bug.

The relation also explains why a deterministic implementation can have a nondeterministic model. The implementation may be deterministic once thread schedule, message arrivals, failures, and inputs are fixed. The model exposes those previously implicit inputs as choices.

Exhaustive checking can explore only the choices the model author made visible.

When determinism is honest

Not every relation needs several successors. Arithmetic evaluation, decoding a canonical byte string, and applying one already selected action may be deterministic. Keeping those kernels deterministic often makes the surrounding choices clearer.

The test is not “could we add nondeterminism?” It is “does the real question depend on a choice not fixed by the current state and selected action?” If no, a function is the more precise model. If yes, forcing one result is information loss.

This separation will return in later tools. TLA+ expresses actions as predicates over two states. Stateright asks a model to enumerate actions and successors. Loom makes thread and memory choices visible through instrumented operations. Different interfaces preserve the same responsibility: the author declares the choice; the engine explores it.

Lessons

A transition relation may admit several next states from one current state.
Nondeterminism preserves unresolved choice; it is not randomness.
Schedules, environment inputs, and failures are common sources of choice.
Exhaustiveness is relative to the actions and successors the model exposes.
Deterministic kernels remain appropriate when the selected inputs determine one result.

Practice

Retrieval. Explain the difference between a random test and a nondeterministic model without using the word “random” in your answer.
Discrimination. A parser maps one fixed byte string to one syntax tree. Should its core parse step admit several next states merely because many users may call it concurrently?
Transfer. A client sends one request and may receive a reply, time out, or retry before the first reply arrives. List the actions a model must expose before it can find a duplicate effect.

Worked answers

A sampled test chooses some paths; a nondeterministic model retains all declared alternatives for the exploration procedure.
No. The parse kernel can remain deterministic for fixed bytes. Concurrency belongs in the caller or scheduling model unless shared parser state changes the result.
At minimum: send, deliver request, apply effect, deliver or lose reply, timeout, retry, and deliver the retried request. Request identity must be state if the service can distinguish repeated delivery.

References

Leslie Lamport. “A High-Level View of TLA+.” 2021. — states, actions, behaviors, and nondeterministic specification
Christel Baier and Joost-Pieter Katoen. “Principles of Model Checking.” MIT Press, 2008. — transition systems, paths, and model-checking semantics

← Keep Only Differences That Change the Future A Bad Future Leaves a Finite Scar →

Two completed jobs are waiting to publish. A test calls publish(A) and then publish(B). The test may be deterministic, repeatable, and green. It has also answered the most important question before the checker arrived: A goes first. A concurrent system does not owe us that order. From the state in which both completions are ready, publication of A and publication of B are both possible next actions. A useful model preserves both edges. The checker follows one, backtracks, follows the other, and continues until it finds a forbidden future or exhausts the declared graph. This is nondeterminism in a formal model. It is not randomness and it does not mean that the system behaves without rules. The rules define a relation: for one current state, several next states may satisfy the action predicate. The model author states the choices; the checking procedure explores them.