I’ll give you my personal approach, but I’m sure others will chime in with much better advice ![]()
I usually am not saving the models I make in Alloy. I tend to treat Alloy like a “mind bicycle” or a design REPL – I described this in another post.
I use the same general structure whether I’m saving the model or not. When I do write a model that’s intended to be shared with others (and ideally maintained in a project), I almost always use Markdown (since that’s a valid file format for the Alloy Analyzer and alloy tool). The typical structure I follow is:
- Write a narrative section to introduce the problem and scope
- Use an Alloy code fence and define the domain objects, their relationships and predicates (or in some situations, facts) that shape the “universe” of the problem. Use Alloy comments to tie the narrative to parts of the model within the code fence.
- Create new markdown sections for critical aspects of the problem or the system you’re describing and repeat the same pattern (narrative explanation, diagrams if helpful, Alloy code fence). These sections of Alloy code are mostly going to be predicates (and in some situations, functions).
- At the very bottom of the markdown file, create one last Alloy code fence where you tie the entire model together (a
stutterpredicate, an init state, all your runs/checks, etc.).
I think many people who work regularly in Alloy use a similar structure. Even generated models (like the ones I mentioned in the other post, eg: spec.md) usually have this format.
Using the Alloy Analyzer (with its Evaluator) makes it possible to explore the entire model and interrogate it as need (no need for Jupyter).