7. A sequence that breaks an invariant

Description

All the construction of lessons 3 to 6 pointed to this moment. You have the complete machine —state, book, cancel, Bundle, three invariants— and you saw it run green against the correct Calendar. Now we do what gives a test meaning: putting it in front of a bug. We recover the book with the all/any error from lessons 1 and 2 —the one that confuses "overlaps with some" with "overlaps with all"— and run the same machine against it. The overlap invariant jumps, and Hypothesis hands us something no single-call test could: the minimal falsifying sequence, shrunk to the three exact operations that reproduce the double booking.

This lesson is about reading and using that report. You are going to see how Hypothesis, just as it shrank an input to the minimal example in module 5, shrinks a whole sequence: it removes the operations that aren't needed, simplifies the arguments of the ones that remain, and leaves you the shortest and simplest history that still breaks the invariant. You are going to learn to read the reproducer —those lines state = CalendarMachine(), bookings_0 = state.book_room(...)— and to reproduce it by pasting it as is into a file to debug. By the end you are going to have the complete cycle of stateful testing in your hands: build the machine, run it, read the failing sequence, reproduce it, and diagnose the bug.

Connection with the module: this lesson adds nothing structural —it uses the complete machine of lesson 6 without changing a line of its shape—; the only thing that changes is the book under test, which now has a bug. It is the culmination of the "catching" part: everything you learned to build, now catching a real defect. Lesson 8, the mini-project, puts you to do this on your own with a different bug. The shrinking you see here applied to sequences is the same concept from module 5, now over a list of operations instead of over an input. We continue with Reservo's Calendar, this time with a broken book.

An analogy: the detective who reconstructs the minimal crime

Imagine a detective in front of a confusing scene: a house with twenty people who came in and out during the night, and at the end a broken object. A bad investigator hands you the complete log —the twenty entries and exits— and tells you "at some point in this it happened." Useless: there is too much noise to see what caused the damage. A good detective does something more valuable: they reconstruct the minimal sequence of events that, on its own, explains the crime. "The twenty people weren't needed. Three were enough: A came in, B came in, and when C came in and pushed A, the object fell. The other seventeen are irrelevant." They give you the shortest history that reproduces the result, and with that the case becomes understandable.

Hypothesis is that good detective, but for sequences of operations. When a long sequence breaks an invariant, it doesn't hand you the long sequence —that would have irrelevant bookings and cancellations, noise that hides the cause. It shrinks: it removes the operations that don't contribute to the failure, simplifies the arguments of the ones that remain (smaller hours, minimal durations), and gives you the minimal sequence that still breaks the invariant. In our case, three bookings —not one more— with the simplest possible values. Just as the detective saves you from checking twenty suspects by pointing to three, Hypothesis saves you from reading a long sequence by showing you the three steps that matter. That reduction is what turns a failure into a diagnosis.

Worked example: the buggy book under the machine

We recover the book_buggy from lessons 1 and 2. The only difference with the machine of lesson 6 is that the rules call book_buggy instead of the correct book; the invariants are identical. Here is the machine, with the bug at the top:

# test_machine_buggy.py -- the SAME machine, against a book with a state bug
from datetime import datetime, timedelta

from hypothesis import strategies as st
from hypothesis.stateful import (
    RuleBasedStateMachine, rule, invariant, Bundle, consumes, multiple,
)

from reservo import Calendar, cancel, overlaps
from reservo.models import Booking
from reservo.schedule import RoomUnavailable

BASE = datetime(2026, 3, 10, 0, 0)
ROOM = "r-focus"


def is_available_buggy(calendar, room_id, start, end):
    confirmed = calendar.confirmed_for_room(room_id)
    if not confirmed:
        return True
    # BUG: "not available" only if the range overlaps with ALL the confirmed ones
    # (all instead of any). With a single booking it behaves well; with two or more,
    # it lets through one that only steps on one of them.
    return not all(overlaps(b.start, b.end, start, end) for b in confirmed)


def book_buggy(calendar, booking_id, room_id, member_id, start, end, price_cents=0):
    if not is_available_buggy(calendar, room_id, start, end):
        raise RoomUnavailable(f"{room_id} occupied in [{start}, {end})")
    booking = Booking(id=booking_id, room_id=room_id, member_id=member_id,
                      start=start, end=end, status="confirmed", price_cents=price_cents)
    calendar.add(booking)
    return booking


class CalendarMachine(RuleBasedStateMachine):
    bookings = Bundle("bookings")

    def __init__(self):
        super().__init__()
        self.calendar = Calendar()
        self.next_id = 0

    @rule(target=bookings,
          start_hour=st.integers(min_value=0, max_value=10),
          length=st.integers(min_value=1, max_value=4))
    def book_room(self, start_hour, length):
        start = BASE + timedelta(hours=start_hour)
        end = start + timedelta(hours=length)
        booking_id = f"bk-{self.next_id}"
        self.next_id += 1
        try:
            book_buggy(self.calendar, booking_id, ROOM, "m-1", start, end, price_cents=1000)
        except RoomUnavailable:
            return multiple()
        return booking_id

    @rule(booking_id=consumes(bookings),
          hours_before=st.integers(min_value=0, max_value=100))
    def cancel_booking(self, booking_id, hours_before):
        booking = self.calendar.get(booking_id)
        now = booking.start - timedelta(hours=hours_before)
        cancel(self.calendar, booking_id, now)

    @invariant()
    def no_two_confirmed_overlap(self):
        confirmed = self.calendar.confirmed_for_room(ROOM)
        for i in range(len(confirmed)):
            for j in range(i + 1, len(confirmed)):
                a, b = confirmed[i], confirmed[j]
                assert not overlaps(a.start, a.end, b.start, b.end), (
                    f"two confirmed overlapping in the same room: {a.id} and {b.id}")


TestCalendar = CalendarMachine.TestCase

What to expect. You run python3 -m pytest test_machine_buggy.py. Red. Hypothesis found a sequence that breaks no_two_confirmed_overlap, shrank it to the minimum, and hands it to you as reproducible code:

$ python3 -m pytest test_machine_buggy.py
=================================== FAILURES ===================================
_____________________________ TestCalendar.runTest _____________________________
E               AssertionError: two confirmed overlapping in the same room: bk-0 and bk-2
E               assert not True
E                +  where True = overlaps(datetime.datetime(2026, 3, 10, 0, 0), datetime.datetime(2026, 3, 10, 1, 0), datetime.datetime(2026, 3, 10, 0, 0), datetime.datetime(2026, 3, 10, 1, 0))
E               Failing test case:
E               state = CalendarMachine()
E               state.no_two_confirmed_overlap()
E               bookings_0 = state.book_room(length=1, start_hour=0)
E               state.no_two_confirmed_overlap()
E               bookings_1 = state.book_room(length=1, start_hour=1)
E               state.no_two_confirmed_overlap()
E               bookings_2 = state.book_room(length=1, start_hour=0)
E               state.no_two_confirmed_overlap()
E               state.teardown()

Reading the reproducer line by line

This block is the most valuable product of stateful testing, so read it calmly. Each line is valid Python code that reconstructs the failure:

• state = CalendarMachine() — creates a fresh instance of the machine (triggers your __init__ with the empty Calendar). It is the starting point of the sequence.
• state.no_two_confirmed_overlap() — Hypothesis interleaves the invariant check before the first operation and after each one. These lines are the detective checking the scene after each event. In an empty calendar the invariant passes (there are no pairs), but Hypothesis includes them so the reproducer is faithful to how it ran.
• bookings_0 = state.book_room(length=1, start_hour=0) — the first operation: books [00:00, 01:00). The result is stored in bookings_0, which is the value that traveled through the Bundle —the booking's id. Hypothesis names that variable to be able to refer to it later if a cancel consumed it.
• bookings_1 = state.book_room(length=1, start_hour=1) — the second: books [01:00, 02:00). It doesn't overlap with the first, so the book_buggy accepts it. Now there are two non-overlapping confirmed: the state the bug needs.
• bookings_2 = state.book_room(length=1, start_hour=0) — the third: books again [00:00, 01:00), on top of the first. It should be rejected (the room is already occupied there), but the book_buggy would only reject it if it overlapped with all the confirmed ones, and it only overlaps with one. It lets it through.
• state.no_two_confirmed_overlap() after the third — here it jumps. The invariant finds that bk-0 and bk-2 occupy [00:00, 01:00) in the same room, and the assertion fails with the message you see above: two confirmed overlapping in the same room: bk-0 and bk-2.
• state.teardown() — the close of the sequence, which Hypothesis calls at the end (although here it already failed before).

The first three lines of the error —AssertionError, assert not True, and the where True = overlaps(...)— are pytest breaking down why the assertion failed: overlaps of two identical ranges [00:00, 01:00) gave True, and the invariant asserted not True. The cause is in plain sight: two confirmed bookings in the same slot.

What makes this report unique is that it is the minimal sequence. Hypothesis doesn't give you the long and noisy history where the failure first appeared; it gives you three book_room —not a cancel, not a fourth booking— with length=1 (the minimum duration) and the smallest hours that reproduce the clash (0, 1, 0). Everything irrelevant was shrunk. It is the detective pointing at the three events that matter.

Reproducing the sequence by pasting it as is

The report is not only for reading: it is executable. You can paste those lines into a file and run them to reproduce the failure deterministically —outside Hypothesis—, which is how a state bug is debugged.

# replay_buggy.py -- paste AS IS the reproducer Hypothesis printed
from test_machine_buggy import CalendarMachine

state = CalendarMachine()
state.no_two_confirmed_overlap()
bookings_0 = state.book_room(length=1, start_hour=0)
state.no_two_confirmed_overlap()
bookings_1 = state.book_room(length=1, start_hour=1)
state.no_two_confirmed_overlap()
bookings_2 = state.book_room(length=1, start_hour=0)
state.no_two_confirmed_overlap()
state.teardown()

What to expect. You run python3 replay_buggy.py and the failure reproduces identical, without Hypothesis in the middle —only the three operations and the invariant check:

$ python3 replay_buggy.py
  ...
  File "/private/tmp/m6work/test_machine_buggy.py", line 74, in no_two_confirmed_overlap
    assert not overlaps(a.start, a.end, b.start, b.end), (
AssertionError: two confirmed overlapping in the same room: bk-0 and bk-2

This is gold for debugging. You have the bug captured in five deterministic lines that run in milliseconds, without random generation, without waiting. You can put a print in is_available_buggy, set a breakpoint, or remove lines to confirm which are necessary —and you will verify that if you remove the second booking (bookings_1), the failure disappears, because without two confirmed the bug doesn't wake up. The reproducer turns a probabilistic failure ("in some random sequence") into a fixed case ("these three operations"), which is precisely what you need to fix it with confidence. And when you fix it —changing all for any in is_available—, this same file will confirm to you that the failure no longer occurs.

Sequence shrinking: what it shrinks and how

It is worth understanding what Hypothesis does to get from a long and random sequence to these three lines, because it is the same shrinking from module 5 operating in a new dimension.

When a sequence fails, Hypothesis tries to simplify it in several ways at once, always keeping the simplest version that still fails:

• It removes operations. It tests whether the sequence without the first operation still fails; without the last; without the middle one. Every operation that can be eliminated without the failure disappearing is eliminated. That is why the reproducer has no cancel or extra bookings: any superfluous operation, Hypothesis removed it. Exactly the three that are needed remained.
• It simplifies the arguments. To each remaining operation, it shrinks the arguments toward the simplest values: length toward 1, start_hour toward 0. That is why the durations are one hour and the hours are 0 and 1 —the smallest values that still produce the clash. It is the same integer shrinking from module 5, applied to the arguments of each rule.
• It reorders and reduces the bundle. Since Hypothesis knows which values of the bundle each rule produced and consumed, it can also simplify that flow, keeping the coherence (not consuming an id that is no longer produced).

The combined result is the minimal sequence: the shortest history, with the simplest arguments, that still breaks the invariant. Note the power of this compared with lesson 2: there we argued that writing sequences by hand doesn't work because, among other things, when they fail they reduce nothing. Here you see the other half of the argument: the machine not only finds the sequence you wouldn't think of (three bookings, two that prepare and one that explodes), but it reduces it to the readable minimum. Finding and shrinking —the two things a battery of by-hand sequences doesn't do— are free with RuleBasedStateMachine.

Common mistakes

Reading the reproducer as just any sequence and not as the minimal one. What happens: someone sees the three book_room and thinks "well, this sequence fails, but maybe it is a rare case." Why it happens: it isn't appreciated that Hypothesis already shrank, so each operation that remained is necessary. How to detect it: if you doubt whether the failure is "important," remember that Hypothesis tried to remove each operation and couldn't without losing the failure. How to fix it: read the reproducer as what it is —the minimal sequence—: each of its operations is indispensable for the bug. If you could remove one and keep failing, Hypothesis would have removed it already. That exactly three bookings are needed is the diagnosis: the bug needs two previous confirmed.

Trying to reproduce the failure by running the machine again instead of pasting the reproducer. What happens: someone, to debug, runs pytest test_machine_buggy.py over and over, and sometimes the failure takes a while or changes shape. Why it happens: they forget that Hypothesis generates different sequences each run (unless it uses its example database). How to detect it: if debugging feels slow or inconsistent, you aren't using the deterministic reproducer. How to fix it: paste the reproducer into a file and run it directly, like replay_buggy.py. That executes exactly the minimal sequence, without randomness, in milliseconds —the ideal environment to put prints, breakpoints and confirm the fix. (Hypothesis also saves the failed example in its database, from module 5, so a re-run usually retries the same one; but the pasted reproducer is the most direct and explicit way.)

Confusing the invariant's message with the root cause. What happens: someone reads "two confirmed overlapping: bk-0 and bk-2" and believes the bug is in the invariant or in overlaps. Why it happens: the failure is reported where it is detected (the invariant), not where it originates (the book_buggy). How to detect it: if you look for the bug in the function that made the assertion jump and don't find it, maybe you are looking at the detector and not the cause. How to fix it: the invariant is the symptom —it tells you the state ended up wrong—; the cause is in the operation that produced that state. Here, the invariant points at the double booking, but the culprit is is_available_buggy (the all instead of any), which let the third booking through. Follow the sequence backward from the symptom to the operation that caused it.

Exercises

Exercise 1

Reproduce the failure: run test_machine_buggy.py and confirm that Hypothesis reports a sequence of three book_room. Then paste the reproducer into replay_buggy.py and run it to see the deterministic failure. Finally, delete the line bookings_1 = state.book_room(length=1, start_hour=1) from replay_buggy.py and run it again. What happens and why?

Exercise 2

Fix the bug: change is_available_buggy so it uses any instead of all (reject if it overlaps with some confirmed). Run test_machine_buggy.py and replay_buggy.py again. What do you expect to see in each? Write the corrected version of the function.

def is_available_fixed(calendar, room_id, start, end):
    confirmed = calendar.confirmed_for_room(room_id)
    # correct: not available if it overlaps with SOME confirmed (any)
    return not any(overlaps(b.start, b.end, start, end) for b in confirmed)

Exercise 3

The invariant that jumped was no_two_confirmed_overlap. The machine of lesson 6 also had count_matches_model. Explain why the count invariant would not have caught this bug, and what that says about having several invariants.

Summary and next step

In this lesson you closed the cycle of stateful testing. You put the complete machine in front of a book with the all/any bug, and the invariant no_two_confirmed_overlap jumped, handing you the minimal falsifying sequence: three book_room with the simplest values (length=1, hours 0, 1, 0) that reproduce the double booking of bk-0 and bk-2. You learned to read the reproducer line by line —state = CalendarMachine(), the bookings_N that travel through the bundle, the interleaved invariant checks— and to reproduce it by pasting it as is into a file, turning a probabilistic failure into a deterministic five-line case, ideal for debugging.

You understood sequence shrinking: Hypothesis removes the operations that aren't needed, simplifies the arguments of the ones that remain, and reduces the bundle flow, giving you the shortest and simplest history that still fails —the same shrinking from module 5, now over a list of operations. And you confirmed, with the count invariant that didn't catch this bug, the underlying lesson: several invariants are needed because each watches a different facet.

Before moving on you should be able to: run a machine against a buggy system and read the falsifying sequence; reproduce the failure by pasting the reproducer; explain what sequence shrinking shrinks; and distinguish the invariant that detects (symptom) from the operation that causes (root).

You already have the whole cycle: build, run, read, reproduce, diagnose, fix. Lesson 8 is the capstone where you do it on your own: you model the Calendar with the complete machine and run it against a variant with a different bug —a cancel that forgets to mark the booking—, which this time gets the count out of sync. You will deliver the machine, the invariants, the falsifying sequence and the diagnosis. It is the synthesis of the whole module. Let's continue.

Resources

• Stateful testing — Hypothesis official documentation — it describes the format of the reproducer a machine prints when it fails and how it is read. The source of this lesson's Failing test case block.
• Shrinking — Hypothesis documentation — the reduction mechanism that, in a machine, shrinks the sequence of operations in addition to their arguments (the same concept from module 5, extended to sequences).
• Rule-based stateful testing (hypothesis.works) — it shows real examples of minimal falsifying sequences and how they are used to diagnose and fix state bugs.