The books on alloy and blog posts reveal a model step by step, by additions and modifications in files, and we have a list of versions: model_1.als, …, model_n.als. I’d like to make this workflow less file-centric and more automated.
I wonder how to structure alloy code in a single file, so that it can be used to illustrate introduced constraints step by step to show how it changes the outcomes.
Would this add too much clutter?
Or maybe it’s better to put this list of developing models in a jupyter notebook and use java api to get visualizations of counterexamples?
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
stutter predicate, 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).
Thank you for the link to the previous discussion. A quote from that thread:
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?”
Yeah, that’s what I’m trying to say. When I use the Alloy UI, all the information gained in the process of building of a model is lost.
I’ve tried already to use alloy in jupyter, it worked, although the setup has to be polished further.
The workflow I have in mind is to generate relevant pictures of counterexamples along with the corresponding textual representations and have them in the notebook for history, because getting back to them is hard when I moved on. It’s just too easy to get lost to me in what I’m doing and from where I’ve come in the process.
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.
Yeah, evaluator and it’s results can be saved in jupyter session as well, this helps to reason about the counterexamples. It’s turtles all the way down.
This is the way I’d like to go, I’m moving forward saving everything as an artifact. I dislike jupyter though, I’d like to replace it later with something that can be stored in git.