Hi all,
Back on the horse of going through this excellent video course.
I had a question and I *think* I know the answer, but would like to double-check, to make sure. :)
In previous videos, system specs would terminate, resulting in a deadlock reached state, and the need to uncheck the deadlock detection box on the model checker. This doesn't happen in the TwoPhase spec.
After inspection, I believe this is because of how the msgs are modeled: In the end state, one of RMRcvCommitMsg(r) or RMRcvAbortMsg(r) will always be true, because any message that's ever been sent stays in msgs forever, which is the only enabling condition for those. Conveniently, this nicely reflects the "at least once delivery" semantics you'd commonly encounter in real systems.
Is this correct, or am I way off?
Also, side question: I've been greatly enjoying these lectures, but I wonder if the
website is still the most up-to-date entry point to them. The videos have been saying, "download the spec and paste it into the module body", as if there's a link I should be seeing on the same screen as the video, but neither the website, nor the video description on youtube, provide any link to these additional materials needed for the lecture. I've found them on github of course, but it leads me to wonder if I'm watching them from the best vantage point. :)
cheers