Bonus Material: Modeling and Verification

Although it is complete overkill, the two properties above naturally call for a more formal treatment of this algorithm. I’m going to use TLA+ and I already apologize for the digression.

We start with the model variables: raw is the environment input, debouncer is a record with the implementation state, and ghost is a specification variable used to precisely define the properties later on.

---- MODULE Dannegger ----
EXTENDS Naturals, TLC, Sequences

VARIABLES
    raw,        \* environment input
    debouncer,  \* record for implementation (ct0, ct1, state)
    ghost       \* ghost queue and state for verification

vars == << raw, debouncer, ghost >>

Init ==
    /\ raw \in BOOLEAN
    /\ \E state \in BOOLEAN:
        /\ debouncer = [ state |-> state, ct0 |-> TRUE, ct1 |-> TRUE ]
        /\ ghost = [ queue |-> <<>>, prev |-> state ]

Init picks an arbitrary value for raw and for the current state. The ladder starts reset with both bits set to TRUE. The ghost variable contains an empty queue and the previous state. The queue tracks the last raw values provided by the environment. The prev state will be used to identify when the debouncer’s state flips.

The debouncer algorithm is pretty much a translation of the C code from before:

\* Implementation step: Dannegger's Debouncer

NextImpl ==
  LET
    i        == debouncer.state # raw
    ct0      == ~ (debouncer.ct0 /\ i)
    ct1      == (ct0 # (debouncer.ct1 /\ i))
    changed  == i /\ ct0 /\ ct1
    state    == debouncer.state # changed
  IN
  /\ debouncer' =
        [ debouncer EXCEPT
            !.state = state,
            !.ct0   = ct0,
            !.ct1   = ct1
        ]

Since TLA+ does not have an infix XOR operator, I used the inequality # operator, which is equivalent here.

To keep this model simple, I decided encoding the next step of environment and ghost variable together.

NextEnv ==
  /\ raw' \in BOOLEAN
  /\ LET q == IF Len(ghost.queue) < 4
              THEN Append(ghost.queue, raw)
              ELSE Tail(ghost.queue) \o << raw >>
     IN ghost' = [ queue |-> q, prev |-> debouncer.state ]

Here, we pick some arbitrary value for the next raw' value. We always append the current raw value to the queue, but when it already contains 4 items, we also drop the oldest item to maintain the queuelength constant.

The combined Next step and Spec definition follow the typical TLA+ pattern:

Next ==
  /\ NextEnv
  /\ NextImpl
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

The most interesting part is the invariants: TypeInv, Safety and Progress.

TypeInv ==
  /\ raw \in BOOLEAN
  /\ debouncer \in [
       state : BOOLEAN,
       ct0   : BOOLEAN,
       ct1   : BOOLEAN
     ]
  /\ ghost \in [
       queue : Seq(BOOLEAN),
       prev  : BOOLEAN
     ]
  /\ Len(ghost.queue) <= 4

Disag(q, v) ==
  /\ Len(q) = 4
  /\ \E b \in BOOLEAN :
       /\ \A i \in 1..4 : q[i] = b
       /\ b # v

Flipped ==
  debouncer.state # ghost.prev

(* Flips only happen after four consecutive disagreements. *)
Safety ==
  /\ Flipped => Len(ghost.queue) >= 4
  /\ Flipped => Disag(ghost.queue, ghost.prev)

(* Four consecutive disagreements cause an immediate flip. *)
Progress == Disag(ghost.queue, ghost.prev) => Flipped

====

TypeInv follows the typical pattern. Safety encodes the first property from above: If a flip occurs, then the last four raw observations must all agree with each other and disagree with the previous state.

Progress is encoded as an invariant because, in this model, it is a stronger statement than mere eventuality. If the queue has 4 observations that disaggree with the previous state, then we must have flipped.