We now use a slightly different configuration (1 producer, 2 consumers, buffer capacity 1) which lets us visually spot the deadlock.

What Changed

Only the configuration changed — the spec is the same. This demonstrates the power of model checking: by exploring different parameter values, we can find bugs that do not appear in simpler configurations.

Try It

Run TLC and notice how the state space grows compared to v02.

State Graph

Slightly larger configuration with which we can visually spot the deadlock:

BlockingQueueDebug.tla/.cfg shows how to interactively explore a state graph with TLC in combination with GraphViz: