We declare Producers and Consumers as symmetry sets to dramatically reduce the state space.
The configuration now uses SYMMETRY to tell TLC that consistently renaming producers among themselves, or consumers among themselves, preserves the model and its properties. This does not discard relationships such as whether the same producer appears twice in the buffer.
Without symmetry, TLC treats "p1 waiting, p2 running" and "p2 waiting, p1 running" as different states. With symmetry, they are equivalent. This can reduce the state space by orders of magnitude.
TLC reduces the complete state space from 57254 to 1647 distinct states. These are the upstream totals for exploration with -deadlock -continue, not the partial counts shown by the browser before it stops at the first violation.
An expression is symmetric for a set S if and only if interchanging any two values of S does not change the value of the expression. You should declare a set S of model values to be a symmetry set only if the specification and all properties you are checking are symmetric for S. Note that symmetry sets should not be used when checking liveness properties.
TLC does not verify that your symmetry declaration is sound. An incorrect declaration can hide errors.
The browser still reports an Invariant violation, but explores fewer distinct states than the previous lesson. Try removing SYMMETRY Sym to compare the runs.
To reproduce the full 1647-state total, save this lesson's spec and configuration locally as BlockingQueue.tla/.cfg, place tla2tools.jar alongside them, and run:
java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue