Learn · All the Ways It Can Break
growing
Ask for the Whole Bounded Trace
A symbolic checker can search every admitted trace through a declared length without enumerating each state first.
You will run paired bounded checks, read a symbolic witness, choose a meaningful length, and write a result sentence that retains the bound. You will also learn why increasing a bound is evidence growth rather than induction.
Run the known defect
The specimen deliberately separates defect and repair:
tla code/all-the-ways-it-can-break/symbolic-capacity/Capacity.tla#bug-and-repair Capacity.tla The repaired action spends capacity only while credit remains.
Run Apalache 0.61.0:
apalache-mc check --init=Init --next=NextBug \
--inv=WithinCapacity --length=3 Capacity.tla
apalache-mc check --init=Init --next=NextFixed \
--inv=WithinCapacity --length=3 Capacity.tlaThe first command must find a counterexample; the second must report no counterexample within the bound. If the first turns green, the negative control has stopped demonstrating the intended failure.
Choose the bound from the failure
A bound should cover a causal hypothesis, not merely fit the clock. The known overflow needs three acquisitions from zero, so length three is a meaningful negative control. If a retry defect needs accept, apply, lose, retry, and apply, a length-three run cannot test it.
Record the shortest plausible witness, the chosen length, solver completion, tool version, and unsupported behaviors. Larger bounds search more prefixes; they do not converge automatically to a theorem.
Lessons
- Symbolic search represents many traces without explicit state enumeration.
--lengthis a semantic boundary on the checked prefixes.- A bound is justified by a causal failure hypothesis.
- A bounded negative control proves the defect is reachable inside the encoding.
- Increasing a bound is not the same as proving an inductive invariant.
Practice
- Retrieval. State the repaired length-three result in one honest sentence.
- Discrimination. Can a length-ten pass establish a property whose shortest plausible witness needs eleven steps?
- Transfer. Determine a bound for overflow after three admissions followed by one delayed release, and justify it from the action sequence.
Worked answers
- No admitted trace of at most three transitions in this typed model violates
WithinCapacity. - No. The hypothesized witness lies outside the checked domain.
- Include every causal step through the violating state; the exact bound depends on whether admission and accounting are separate actions.
References
- Apalache team. Bounded model checking. — symbolic traces and length bounds
- Apalache team. Running Apalache. — command-line checking options