Motivating Example
The Venezuelan car manufacturer "Sucre" has been developing a futuristic electric car, called the
Quipos.
The Quipos has only three digital control circuits:
the Energy Control Circuit (ECQ),
the Wheel Control Circuit (WCQ), and
the Human Haptics Detection (HHD) circuit.
During development one of the circuits was repeatedly sending faulty signals to the WCQ, causing
it to fail, with corresponding downstream impact on the car's self-steering and automatic braking
features.
The engineers needed to determine: Which circuit is sending the faulty signals to the
WCQ?
The following facts are known about the signals being sent between the circuits:
- A sending circuit causes a receiving circuit to fail by sending it (faulty) signals.
- A sending circuit never uses more power than the receiving circuit.
- The ECQ never sent signals to circuits that the WCQ sent signals to.
- The WCQ sent signals to all the circuits except the HHD.
- The HHD sent signals to all the circuits that did not use more power than the WCQ.
- The HHD sent signals to all the circuits that that the WCQ sent signals to.
- No circuit sent signals to every circuit.
Automated Theorem Proving was used to analyse this issue, and it turned out that
...
the WCQ was sending faulty signals to itself, causing
itself to fail!
Another version