Aclassifier

> Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.

I thought CSPm/FDR4 proved liveness on infinite event trails without temporal logic? Can't one extract "never" and "sooner or later" by just exploring the whole state space? Deadlock/livelock will never happen etc.

I watched this very interesting and amusing series of videos and learned a lot from them. I was shown practical in-use and the motivation for mathematical syntax. I know Promela and CSPm some so I was curious to see more than a trivial example of some C lines becoming a TLA+ spec. I missed real-life examples of down-to-earth usage. The "Formal Development of a Network-Centric RTOS" book shows not only TLA+ but also why in their situation TLA+ was more suitable then other methodologies. Still, on TLA+ I miss the forest for the trees. I probably need more time with Lamport. I hope he's able to do a follow-up. (Or am I unfair here?)