Now we infer the inequation under which the system is deadlock-free.

What Changed

The spec and config are extended to systematically check when the deadlock invariant holds and when it does not.

Key Insight

TLC finds that the system is deadlock-free when BufCapacity >= (Producers + Consumers - 1). This is a precise characterization discovered through model checking.

We run TLC with the -continue option to not stop state space exploration after a violation has been found, asking TLC to find all violations. A bit of analysis reveals that BlockingQueue is deadlock-free iff 2*BufCapacity >= Cardinality(Producers \\union Consumers).

Collecting even more data, we can correlate the length of the error trace with the constants: