You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · All the Ways It Can Break

growing

Read the Trace Backward

The final bad state names the symptom; the enabling actions explain the defect.

formal-methods, tlc, counterexample, debugging, trace, learn

You will translate a TLC state sequence into domain actions, compute one delta per step, identify the earliest causal divergence, and test a repair with both a negative control and a positive witness.

Four states after the initial state

The relevant trace reads:

queued, {}, {}
running, {}, {}             Start(job_a)
running, {job_a}, {}        Cancel(job_a)
complete, {job_a}, {}       Complete(job_a)
complete, {job_a}, {job_a}  PublishBug(job_a)

Do not begin with every printed value. For each adjacent pair, list only the coordinates that changed. Then find the action whose primed formula produces that delta and whose unprimed guard is true in the preceding state. This makes the label checkable rather than trusting a line number.

Diagnosis — choose the earliest action whose permission contradicts the intended policy.

Minimize by meaning, not only length

The shortest trace is helpful, but the smallest explanatory trace matters more. Remove an action mentally and ask whether the remaining sequence can still establish its guards. Without start, cancel is disabled. Without cancel, the invariant is not violated. Without complete, publish is disabled. Each step carries causal information.

For a larger trace, project away variables irrelevant to the violated observation, then retain the guards that justify each transition. This is a manual trace slice. It can reveal that a noisy retry counter never affected the failure while an overlooked generation identifier did.

Repair, rerun, mutate

After adding the guard, rerun the fixed configuration. Then perform two checks:

  1. an uncanceled job can still reach published; and
  2. removing the guard again restores the same counterexample family.

The first rejects overconstraint. The second keeps the checker and property wired to the defect. Finally, change a nearby rule—permit cancellation after completion, for example—and predict whether the invariant still holds before running TLC.

Lessons

  • The final state identifies a symptom; state deltas and guards identify cause.
  • Read a trace backward to the earliest wrongly enabled action.
  • Preserve domain history needed to explain why a state is forbidden.
  • A good repair retains useful positive behavior.
  • Rerunning a known mutation proves the diagnostic remains live.

Practice

  1. Retrieval. Reconstruct the four action names in the failing order.
  2. Discrimination. Why is a state constraint excluding canceled jobs from completion not equivalent evidence to guarding publication?
  3. Transfer. A duplicate debit trace is accept, debit, lose reply, retry, debit. Identify the earliest action that needs request identity.

Worked answers

  1. Start, cancel, complete, publish.
  2. It removes cleanup behavior and checks a smaller lifecycle rather than the intended policy.
  3. The first debit must record the request identity, and retry must consult it before applying another irreversible effect.

References

  1. Leslie Lamport. Specifying Systems, Chapter 14. — TLC error traces and model checking
  2. TLA+ Foundation. TLA+ documentation. — Toolbox and command-line trace workflows

← Give the Infinite Language a Finite Model Make the State Space Pay Rent →