[ohpauleez]

This largely sums up my experience with Alloy and TLA+, as well as when I favor using one tool over the other. My formal education included classes in Z, so the spirit of Alloy always made sense to me and it's usually the tool I start with (I tend to see systems problems as relations, the tooling is fantastic, the REPL is very useful, counter-examples help illuminate the problem space, etc.) When my problem is strictly algorithmic or it's all about the evolution of state spaces over time (especially concurrent states over time), I lean towards TLA+.

When my problem is strictly a state machine, I usually write out some combination of a Parnas table and a statechart, and then encode the table into Alloy.

I have a little tutorial I use to teach teammates the basics of TLA+ and Alloy, which takes about two hours to get through. I find that within a week of using Alloy, folks are dangerous enough to get value out of it.

[jplane]

Is the "little tutorial" available somewhere? I'd be interested in working through it.