We declare Producers and Consumers as symmetry sets to dramatically reduce the state space.
The configuration now uses SYMMETRY to tell TLC that individual producer/consumer identities do not matter — only the count matters.
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 can take advantage of symmetry sets to reduce the number of distinct states it has to examine from 57254 to 1647!
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.