Hi Hillel!
Thanks for getting back to alloydocs and helping build up material for others!
I use Alloy in my day-to-day at work (I have for many years) and maintain some educational materials I use internally at work to help others get up to speed on Alloy (and TLA+) – they predate your alloydocs and wonderful TLA+ book.
Reflecting on my own personal usage, there are a few things I think are worth highlighting in materials:
- Working in Alloy is more like riding a “mind bicycle” - I use it as an interactive, iterative design REPL. I don’t know of anyone who writes a model in one go. I tend to see most people model a little, have Alloy generate some pictures, spot things that wrong, model a bit more, etc. I then turn the model around and ask questions, “Can an X ever be present when a Y is present?” We use Alloy to amplify our thinking, treating it more like a cognitive computing tool. I probably keep less than 10% of all the models I create because the models don’t necessarily have value, the process of creating the model is the valuable part.
- I never start the design process with Alloy, I first draw some informal pictures to get a sense of the problem and focus my catalytic questioning, then I jump into Alloy. I think a lot of beginners jump into Alloy immediately and get frustrated by how slow/cumbersome it is to express their thoughts (mostly because they don’t know what their thoughts are yet and Alloy is poor medium for finding your ‘first thought’). Showing beginners a path or “way of working” gets them to results/rewards/feedback quicker.
- This next one is very specific to Systems work, but I think it generally applies to most situations: Once I have a domain/relational model of my problem, I very quickly move into describing a state machine. Giving people great exemplars to build from is very useful. In my own materials, readers build progressively more complex state machines (flip-flop switch, bounded buffer, async channel, a public library, etc. – It ends with a model of viewstamped replication). Focusing on how to make great state machines in Alloy (especially Alloy 6) is very useful and its important to highlight the patterns, the way to inspect traces, etc.
- I know it doesn’t get a lot of attention but the Alloy Evaluator can be very useful, and highlighting ways to make the most of it is useful for new users.
Cheers,
Paul