What a counterexample is

Of all the reports that come back from the field, this is the one that gives you the most trouble.

“It stops sometimes.”

There are no steps to reproduce it. There are logs, but they only show you what surrounded the stop. In front of you, the machine is running perfectly normally. You cycle it dozens of times and it never stops. And yet the report exists, and a corrective action has to be written.

What you actually want at that moment is not the name of the cause. It is the order. What happens, and what happens after that, to arrive at that state. Once you know that, the rest is not much of a job.

The errors we are used to don’t tell us the route

Errors reach you in roughly two forms.

One is the field report. “It stops sometimes.” “An alarm comes up occasionally.” You know the symptom; you don’t know the route.

The other is a failing test. “assertion failed”. You know which condition broke, and on which line. But you don’t know why execution ever got there. From the input the test supplied onwards, you trace it yourself.

Both of them tell you the broken result. Neither tells you the road to the breakage.

Verifying a design is different here. You write into the design that “while the door is open, no moving part is in motion”, and you have a machine check exhaustively whether that actually holds. When it does not, what comes back is not a one-line “it does not hold”. What comes back is the sequence of events that makes it stop holding, laid out in order. That is what we call a counterexample.

A counterexample is a reproduction procedure, generated automatically.

Walking through one counterexample

Take a textbook machine: a transfer arm, a Z axis, and a door interlock — an unremarkable configuration.

One safety condition.

While the door is open, no moving part is in motion.

Put this through verification, and you get back a sequence like this.

1. Initial state: door=closed, Z axis=upper limit, transfer=idle, interlock=released
2. Operator presses the door-open button  → door=opening (mechanically starts to move)
3. Host commands transfer start           → transfer=running
4. Door sensor detects the open state     → door=open, interlock request issued
5. Interlock requests a stop              → transfer=decelerating

Violation: at step 4, door=open and transfer=running
           safety condition "while the door is open, no moving part is in
           motion" is broken

The place to read is between step 2 and step 4.

Between the door-open button being pressed and the door sensor detecting the open state, there is a gap. On paper the design looked like a single line: door opens → interlock → stop. In reality the button and the detection are separate events, and a command from the host can slip in between them. The counterexample shows you one concrete procedure that goes through that gap.

From here on it is ordinary design work. Do you raise the interlock request at the moment the button is pressed? Do you gate the host’s transfer-start command on the door state? Do you rewrite the safety condition to include the time a stop takes? Which one you choose is a design judgement, but what needs to be discussed is already in your hands.

”Design problem or implementation problem” disappears

What costs money when debugging a machine is not the time spent fixing it. It is the time spent working out where the fault is. And the first step of that is always this —

“Is this a design problem or an implementation problem?”

A counterexample skips that question. What a counterexample shows is not an implementation bug. It is the fact that the design permits that procedure. That is settled before you have read a single line of code, without ever touching the physical machine.

The difference between “something is wrong somewhere” and “it goes wrong when it happens in this order” is worth weeks of debugging.

The fact that it can be reviewed

The most practical property of a counterexample is probably this. A human can read it.

What comes back is not the internals of a proof, nor tool-specific notation. It is a sequence written in the vocabulary the design already uses — signals, states, transitions. So it goes straight into a design review. Put it on the screen, trace it from the top, and explain: here is where the transfer starts moving; here is where the detection arrives.

This is an entirely different thing from “the tool says there is a problem, please trust it”. A counterexample is not a claim; it is a procedure. A procedure can be checked by everyone in the room. To judge whether a counterexample is valid, you do not need to understand the verification. Understanding the machine is enough.

And once you have the sequence of events, it is a test case as it stands. When the physical machine exists, operate it in this order and confirm. It can also be kept as a regression scenario after the fix. A counterexample is not a one-off remark; it has the shape of something that stays behind as an asset.

When a counterexample points at the model rather than the design

Let me put this honestly.

You will read a counterexample and think, this procedure could never happen on the real machine. It happens often. And that instinct is frequently right.

There are usually two causes.

One is that the safety condition was written wrong. In “while the door is open”, did “open” mean the button being pressed, or the sensor detecting it? Write it while it is still ambiguous and you get back sequences that follow a reading you never intended.

The other is that the model was too loose. Two events that mechanically cannot happen at the same time on the real machine were left independently possible in the model. Then procedures that do not exist in reality come back as counterexamples.

Neither is a failure. In both cases what you have learned is that you had not written your design precisely. Design documents that have run for years with “what counts as open” left vague are not rare. A counterexample puts that vagueness in front of you in the shape of a concrete procedure.

That said, this too needs saying plainly. Reading counterexamples is a skill. At first, telling a design error apart from a model error takes time. Read a few and you get used to it. Until you do, it takes as long as it takes.

Finite sequences, and loops that never end

One footnote.

Counterexamples come in two shapes, depending on the property you want to confirm.

For conditions of the “nothing bad happens” type — no moving part moves while the door is open, two axes never enter the interference zone at the same time — a violation comes back as a finite sequence of events leading to the bad state. The example above is this kind.

For conditions of the “something good eventually happens” type — commanding a return to home always reaches home, recovery from an emergency stop is always possible — a violation comes back as a loop that keeps going round without the good thing ever happening. It shuttles between two states and never arrives at home. On a machine, that is a hang.

You read both the same way. From the top, following the events in order.

What to read next

You get a counterexample back because the investigation is done differently from testing. A test tries the procedures you chose; design verification examines the procedures as a whole. That difference is covered in What is the difference between testing and formal methods?.

And why equipment software had no choice but to lean on the physical machine in the first place — that structure is in Why equipment software cannot run the right-hand side of the V-model.