4 ms·

It'd be cool to see this, and the fix, modeled in TLA+

• hwayne 6y ago
  plz stop nerdsniping me More seriously, I'd love to see this modeled in Promela/Spin. There was a go bug a while back where I reproduced it in TLA+ and someone else reproduced it in Spin, and I personally liked the Spin solution a lot more. It seems well-suited for these kinds of problems!
  • nsm 6y ago
    Haha! My very first thought on reading the parent comment was "Hillel Wayne would be all over this!"
  • Bjartr 6y ago
    Haha, sorry. Although I will say your blog is precisely where my interest in TLA+ originated from.