In this step, we convert some constants into variables to explore a wider range of configurations automatically.
Instead of fixing the buffer capacity as a constant, the spec now allows TLC to explore different values. This lets us check the invariant across many configurations in a single run.
Converting constants to variables is a powerful technique: it lets TLC explore configurations you might not have thought to check manually.
As Michel Charpentier points out, BlockingQueue is deadlock-free under some configurations, but model checking is not helpful with finding the underlying mathematical function. However, we can at least ask TLC to find as many data points as possible. This rewrite increases the complete state space to 57254 distinct states, but TLC continues to find the deadlock behavior.