This repo contains the specifications for testing the problems presented on the site "The Deadlock Empire" https://deadlockempire.github.io/
I have always referred students to this site to learn about concurrency and deadlock, and now as I am learning TLA+ I found the problems stated on this site to be extremely useful test cases for specifying systems which exhibit deadlock and using the TLC model checker to identify how deadlock will occur.