search

lemmy / BlockingQueue

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
https://youtu.be/wjsI0lTSjIo
MIT License
485 stars 21 forks source link

Questions about "Weeks of Debugging Can Save You Hours of TLA+" #1

Closed PineWu closed 4 years ago

PineWu commented 4 years ago

Hi, Kuppe: I have read your great talk presentation from here： https://bitbucket.org/lemmster/blockingqueue

But I have a little confused about the state graph in “BlockingQueue in PlusCal” section，as attached. image

Highlighted in red box. If the "p1" is already in the waitset, the 'put' action should not occur because we have only one producer and it is blocked now. PS: the state graph in this git project has no such action.

I’m not sure if my understanding is correct or if that PDF is out of date. Please help. Thanks

lemmy commented 4 years ago

Thanks for reporting, the PDF at bitbucket is outdated. To avoid future confusion, I made that repo private.

PineWu commented 4 years ago

Got it, thanks