Planning on getting back to working on alloydocs this summer and updating it with Alloy 6 (finally!) Are there any other topics you’d like to see covered as either reference material or as tutorials/topics/examples/etc?
1 Like
My take on situation:
Don’t put your effort into the documentation nobody will read. Focus on popularizing Alloy to generate activity instead. People will tell you what they don’t understand, then you can document that
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
2 Likes
This is exactly how I use Alloy in practice! I also start an Alloy when I am learning something new. I am a sucker for cardinalities and Alloy allows me to model my understanding. And yes, I also have mostly unfinished models … it is the thinking process that counts.
I’ve been pondering about a combination with AI like GPT to get the mind straightened out and something like Alloy to record the actual definitions.
I forgot to mention in my original message-
I’m more than happy to help out with the effort in anyway you like – coauthor material, review, hand over some of my own material for you to crib from, anything!
Some more thoughts:
- It can be motivating for new users to see all the interesting things folks have done with Alloy: TestEra (using Alloy as a test oracle for testing Java programs), Automated SQL generation for testing database engines, using Alloy as a testing oracle for train stations and switching, the often-cited cases of folks finding bugs in protocols when modeling the systems in Alloy, etc. I think many newcomers look at Alloy and think, “that’s a tool for building models, end of story,” and it’s up to us to illustrate the utility and versatility of the tool (to help expand their conceptual ‘world view’).
- It can be exciting to newcomers to see how active Alloy development is. I’m specifically thinking of the great work by Allison Sullivan and the SCOPE lab ( Projects - SCOPE Lab ), Nancy Day and others at Waterloo WatForm, obviously the folks at Haslab, the automated model repair work in BeAFix, etc.
I think a few really exciting areas for me personally are:
- Hole-based Alloy / Alloy model synthesis by Sullivan
- Live programming of Models with ‘implication’ by Sullivan ( https://arxiv.org/pdf/2305.17317.pdf ), which I really hope sets the direction for the main Alloytools distribution (or the Alloy VSCode extension).
- Better programmatic access to Alloy from Java for easier differential testing, model-checker guided distributed systems testing, augmenting metamorphic testing – TL;DR where Alloy lives across the entire SDLC from design through software aging/maintenance
- Making the bridge into Alloy a bit easier by representing Statecharts directly in Alloy (ala the Dash+ line of work)
Regards,
Paul
(ps- apologies for not linking all the labs and work. As a new user I’m only allowed to put in two links)
1 Like
In reference to “value is in making the model, not necessarily the model itself”
I think the way Ankush Desai talks about P provides a lot of inspiration (and resonates with a large audience, including those who are new to formal methods): "Formal Modeling and Analysis of Distributed Systems" by Ankush Desai (Strange Loop 2022) - YouTube
For me, one of the hardest parts about understanding Alloy has been figuring out what to ignore: For example, there are 3 different ways to model sequences, and some of them appear pretty well obsolete.
Also, a very careful description of how the temporal operators work - with diagrams - would be greatly appreciated. Their behavior is really subtle - I still don’t understand “triggered” hardly at all. There were errors in the descriptions on the alloytools site, and there’s hardly anything to speak of on alloydocs.
The behavior of int casting is confusing as well.
Overall, in my opinion, the parts that need the most documentation are the parts that defy an intuitive understanding of how Alloy ought to work. BDFL Daniel Jackson wrote a book on The Essence of Software that describes scenarios where the conceptual model of the user doesn’t match with the model that the software implements, with disastrous results. That’s all to say that rectifying users’ conceptual models of Alloy is most important, I think, rather than just giving examples of basic usage.
1 Like
This is an excellent suggestion. Maybe we should start a thread where people can disclose their conceptual mismatches about the language and explain how those made it difficult to master it.