Deadlock
Deadlock
Deadlock is generally considered to happen only in multiprocess
algorithms. It results from each process waiting for another
process to do something. But when algorithms are viewed
mathematically, which is how TLA+ views them, the halting of an
execution because of a with (i \in {}) statement looks
the same as halting because of deadlock. They are both instances
of a system waiting for something that can never happen.