Consider adding a more explicit section on "deadlocks" in TLA+

hwayne / learntla

A TLA+ guide

http://www.learntla.com

Creative Commons Attribution 4.0 International

278 stars 57 forks source link

Consider adding a more explicit section on "deadlocks" in TLA+ #103

Open will62794 opened 3 years ago

will62794 commented 3 years ago

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.

hwayne commented 3 years ago

I'll be doing a complete rewrite of the site in 2022, def gonna cover it then!

will62794 commented 3 years ago

Sounds good, thanks!

hwayne commented 2 years ago

Leaving this and the other open because they're still good additions to V2