In this step, we convert some constants into variables to explore a wider range of configurations automatically.
The constants now bound the choices for three new variables: producers, consumers, and bufCapacity. Init chooses nonempty subsets of the process sets and a capacity in 1..BufCapacity. Next leaves these variables unchanged, so each behavior uses one fixed configuration rather than changing its configuration while running.
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. TLC can supply data points from finite models to help us infer a general relationship, but those data points are not a proof for unbounded parameters.
The browser still reports an Invariant violation and stops at the first counterexample. There are 315 initial states for the supplied bounds. Try reducing the sets or capacity bound to see how many initial configurations remain.
The complete state space has 57254 distinct states, as reported upstream. To explore it past invariant violations, save this lesson's editors as BlockingQueue.tla and BlockingQueue.cfg alongside a local tla2tools.jar, then run:
java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue-continue continues after invariant violations; -deadlock disables the separate built-in deadlock check so it does not stop the run. The invariant still reports all-waiting states. These options are not exposed by the browser playground, whose partial state count will be smaller.