Upstream v11 tries an additional, non-deterministically scheduled notification as a workaround for the blocking-queue bug. It is an attempted fix, not the final solution.
Notify already used \E x \in waitSet to choose any waiting thread. The new choice is in Next: notification can now happen as a separate step, without a producer adding an item or a consumer removing one.
As the upstream tutorial explains, we can keep waking the wrong kind of thread, which cannot perform useful work and goes back to waiting. Adding a possible wakeup does not guarantee progress.
There is an important distinction in this version: Invariant still forbids all threads being in waitSet, but that state is no longer a TLC deadlock. The independent Notify step remains enabled and can wake someone. Even when waitSet is empty, that step permits an unchanged state.
The supplied invariant checks a state condition, not eventual progress. A liveness claim would require a temporal property and appropriate fairness assumptions; upstream explores these in later lessons.
TLC reports an Invariant violation because all threads can still be waiting. Try removing only INVARIANT Invariant from the configuration: TLC completes without a built-in deadlock error, but that does not establish that useful work must continue.