A critical bugfix: the notification mechanism now non-deterministically selects which waiting thread to wake up.
Previously, the spec assumed a specific thread would be notified. Now it models the real behavior of notify() in Java: any one of the waiting threads can be selected.
If we always notify a specific thread, we miss executions where a different thread gets notified — which could lead to deadlock.
When modeling a system, you must capture all possible behaviors, not just the ones you expect. Non-determinism is how TLA+ models situations where the system can make any of several choices.
Non-deterministically notify waiting threads in an attempt to fix the deadlock situation. This attempt fails because we might end up waking the wrong thread up over and over again.