How to tell a story using alloy models?

Questions
1

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?

2

I’ll give you my personal approach, but I’m sure others will chime in with much better advice :slight_smile:

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).