1
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:
https://github.com/rodgarrison/tla_note1
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.
In the paper:
- program behavior versus model states
- deadlock
- termination
- coverage (label) checks
- setting up TLA+ on the command line
Hope it helps. As I note in the abstract I got some help of my own from the TLA Google Group.
But ... but ... this 2019 Macbook has %^#$#@ GD ^&&^$%@#@# piece of ^&%^#$ control strip.
Almost every time my fingers move too close to the strip the software "HELPS me" by changing desktops, applications, and all other manner of complete BS. I have yet to find how I can disable it from having a context sensitive menu.
This is what I think stands up the FSF, FOSS, and some of the push back on Ubuntu's new package manager. If the supplier wants to innovate their way - more power to them. But provide an opt out option for God sakes. The enlightened Nanny state is something that at least for me, is wholly intolerable.
Apple has a lot of overpaid, and under utilized programmers apparently: they've wormed themselves into every possible interaction in all permutations of all power sets of all keyboard, mouse, track pad scenarios so that if you blink wrong it runs Reddit for you. Fuck that.
After I wrote about this, and got that off my mind, I think I fixed it. But geez it wasn't obvious. So Apple, it wasn't so onerous. I guess I have some responsibility here too.