I use the term brainwash as satire. Of course, the programmer imperative sensibility is quite important if you want to ship product, which is the bottom line.<p>But I've found the imperative mentality in my own work on TLA+ modeling initially confusing. I offer the following write-up to help clarify several important points (focusing on TLA+ Pluscal) in a technical note with example models, Python code. It's the first in a series on modeling a distributed key-value store I'm working on:<p>https://github.com/rodgarrison/tla_note1<p>Beyond basics I also give a recipe to use TLA+ at the command line for those of us who prefer it over IDEs. TLA's toolbox IDE is nice; still I prefer command line development when possible.<p>In the paper:<p>- program behavior versus model states<p>- deadlock<p>- termination<p>- coverage (label) checks<p>- setting up TLA+ on the command line<p>Hope it helps. As I note in the abstract I got some help of my own from the TLA Google Group.