I've been learning TLA+ for the past two months, hoping I could use it as a formal language for software design generally and not just for concurrent systems. I'm enamored with the idea of using math formalisms to describe a state machine.
But now that I've gone through Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at
But now that I've gone through Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at
https://github.com/tlaplus/Examples/tree/master/specificatio...
I'm less sure now that I can. I'll keep plugging away, but if anyone here has any suggestions or offers any alternatives, I'm all ears.