A debug configuration with 2 producers, 1 consumer, and buffer capacity 1.

What Changed

Again just a configuration change. Different configurations expose different behaviors. The deadlock might be easier or harder to find depending on the number of producers and consumers.

With the help of TLCExt!PickSuccessor we build us a debugger with which we study the state graph interactively. We learn that with configuration p2c1b1 there are two deadlock states: