Try as I may, I just cannot get my head around how to think in order to produce specs in PlusCal / TLA+. I really wish I could because I feel that it could yield enormous benefits for me & my colleagues at work, and of course it would be a handy tool to have in the toolbox for the future.
To start out, you can just think of it as a nice DSL for specifying a finite state machine. Every action defines a state transition, and unprimed variables are the guards - if they are true of the state you’re in then the transition can be taken. And the primed variables will be the values of your variables in the next state. Thinking of your program as a state machine is pretty powerful, and even intuitive for many people! Then you can define invariants that must stay true in every state, and the model checker can check that. Also all variables are global, which people find weird, until they realize how valuable a single consistent view of the entire system is for writing & checking invariants.
Once you start caring about liveness (good things eventually happen, checked with temporal properties) in addition to safety (bad things don’t happen, checked with invariants) you will have to augment your understanding beyond the state machine model. But 90% of people really only need and use safety checking, where the state machine mental model is all you need.
@hwayne made the website https://learntla.com (and your company can hire him to lead a workshop teaching you & your coworkers about the language!) and there is also a video course made by Leslie Lamport. Personally I learned from the book Specifying Systems but that was a decade ago and many things have been made since then: http://lamport.azurewebsites.net/tla/learning.html
Try as I may, I just cannot get my head around how to think in order to produce specs in PlusCal / TLA+. I really wish I could because I feel that it could yield enormous benefits for me & my colleagues at work, and of course it would be a handy tool to have in the toolbox for the future.
To start out, you can just think of it as a nice DSL for specifying a finite state machine. Every action defines a state transition, and unprimed variables are the guards - if they are true of the state you’re in then the transition can be taken. And the primed variables will be the values of your variables in the next state. Thinking of your program as a state machine is pretty powerful, and even intuitive for many people! Then you can define invariants that must stay true in every state, and the model checker can check that. Also all variables are global, which people find weird, until they realize how valuable a single consistent view of the entire system is for writing & checking invariants.
Once you start caring about liveness (good things eventually happen, checked with temporal properties) in addition to safety (bad things don’t happen, checked with invariants) you will have to augment your understanding beyond the state machine model. But 90% of people really only need and use safety checking, where the state machine mental model is all you need.
@hwayne made the website https://learntla.com (and your company can hire him to lead a workshop teaching you & your coworkers about the language!) and there is also a video course made by Leslie Lamport. Personally I learned from the book Specifying Systems but that was a decade ago and many things have been made since then: http://lamport.azurewebsites.net/tla/learning.html