Exploring the NaiadClock TLA+ model in TLA-Web
I have been impressed by the usability of TLA-Web from Will Schultz. Recently I have been using it for my TLA+ modeling of MongoDB catalog protocols internally, and found it very useful to explore and understand behavior. This got me thinking that TLA-Web would be really useful when exploring and understanding an unfamiliar spec I picked up on the web.
To test my hunch, I browsed through the TLA+ spec examples here, and I came across this spec about the Naiad Clock. Since I had read DBSP paper recently, this was all the more interesting to me. I had written about Naiad in 2014, and about dataflow systems more broadly in 2017.
Unfortunately, I would not be able to play with the spec, because it only came in paper form: "The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof." The spec was available only as 13 pages of latex symbols in the Appendix A of this paper. I did briefly consider manually transforming this to the ASCII version by spending 2-3 hours, but then I remembered I am lazy, ADHD, and hahaha it is so funny that I even considered I could do this. Then I had a thought. What if I give this pdf to ChatGPT and asked back the ASCII version. Lo and behold that worked almost flawless, and in less than a minute's work!
I was so impressed that I tweeted about what a marvel this is. This could be a great way to salvage some TLA+ specs that only appear in latex formatted pdf publications.
