This repository was archived by the owner on Jul 2, 2022. It is now read-only.
Consider adding a more explicit section on "deadlocks" in TLA+ #103
Description
People often seem to get tripped up by the semantics of what a deadlock is in TLA+ and how TLC checks for it. For example, see this thread and this thread. To help avoid the same confusion for others in future, might help to include a more explicit section covering the notion of deadlock in TLA+. A note does appear here in the section on processes, but it might be easy to miss if you're looking for details about deadlocks specifically.