43 pointsby ingve9 months ago1 comment
  • edvardas9 months ago
    Succinct and rigorous. This article has a clear problem statement, explicitly calls out assumptions and expected properties, shows how to express them in TLA+/PlusCal, and even adds a sanity check by refining the mutex model. I wish I had seen this article when writing my BA thesis.