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.
1 comment
[ 7.6 ms ] story [ 48.9 ms ] thread