Hey everyone I’ve just started playing around with Alloy and I have a few beginner questions.
Context
To start off with, let’s say I’m trying to model something near and dear to my heart (and liver): whiskey. I think about this as follows:
- A bottle of whiskey is essentially its contents, so we’ll model the contents.
- The contents of a whiskey is made up of a blend of one or more “maturations.”
- A maturation is a relation between a distillate (the distilled liquid) and a barrel.
- A distillate is a particular batch of liquid, and as such should only appear in a single barrel at a time.
At some point I’d like to model the fact that you can take the liquid out of one barrel, split it into different batches, mature each of those batches in separate barrels, then blend those batches together along with a completely different distillate that came from somewhere else. In short, the maturations that make up the contents of a whiskey form a directed acyclic graph. I want to get here eventually, but we’ll set this part aside for the moment.
The first pass I made at modeling the bulleted list above looks like this:
-- It's a barrel
sig Barrel {}
-- The distilled liquid
sig Distillate {}
-- A period of time that a distillate spent maturing in a particular barrel
sig Maturation {
barrel: one Barrel,
distillate: one Distillate,
}
-- Simplified contents of a bottle of whiskey
sig Contents {
maturations: set Maturation
}
Workflow
As you can imagine, with no checks, facts, etc defined you get nonsense if you run this.
Question: Which parts of the model do you encode as facts, which do you encode as predicates, and which things do you check?
Seeing that the unconstrained model produces nonsense, it’s easy to identify a few constraints, such as:
- A distillate should only be found in a single Maturation
- A maturation should only be found in a single Contents
- A Barrel should be found in some Maturation (barrels can be reused)
I’ve written these down as predicates:
pred distillate_found_in_maturation[d: Distillate] {
one m: Maturation | m.distillate = d
}
pred barrel_found_in_maturation[b: Barrel] {
some m: Maturation | m.barrel = b
}
pred maturation_found_in_contents[m: Maturation] {
one c: Contents | m in c.maturations
}
pred no_orphans {
all d: Distillate | distillate_found_in_maturation[d]
all b: Barrel | barrel_found_in_maturation[b]
all m: Maturation | maturation_found_in_contents[m]
}
I’ve created a predicate no_orphans that tie these three other predicates together as well. I called this no_orphans because I first identified that without constraints you got distillates not found in maturations, maturations not found in contents, etc.
At this point do you just run { no_orphans } and inspect the visualization to see that it makes sense? Is there a more idiomatic way to say “these are the logical constraints I’ve identified, check that there are no logical errors”?
Visualizer
If I run the visualizer with the above predicates and run { no_orphans } I get the following result:
Question: What are the $barrel_found_in_maturation_m connections and how do I hide them? They obviously have a similar name to one of the predicates, so I suppose they’re related somehow, but they just seem to point the opposite direction of the maturation->barrel relation and generally clutter up the visualization.
DAG
Now let’s say we come back to wanting to model blending different batches of distillates. I think the way I’d model this is:
- A distillate can be produced by blending multiple maturations
- A maturation can be split into multiple distillates
So, I would model this as follows:
-- The distilled liquid
sig Distillate {
blended_from: set Maturation
}
-- A period of time that a distillate spent maturing in a particular barrel
sig Maturation {
barrel: one Barrel,
distillate: one Distillate,
split_into: set Distillate,
}
My first constraint would be to enforce that every Distillate split out from a maturation must then belong to a new Maturation. In pseudo-code that would look like:
for any Maturation m:
for any Distillate d:
if d in m.split_into:
d belongs to some maturation
I’m not confident I know how to model that in Alloy, but this is what I came up with:
pred splits_belong_to_maturations {
all disjoint m1, m2: Maturation |
all d: Distillate |
d in m1.split_into implies m2.distillate = d
}
Question: Is this how you would model that?
Next I’d want to model the constraint that there are no cycles i.e. no Distillate is split into a Maturation that will somehow be blended together to make the original Distillate.
This I have no idea how to do. My intuition says that there’s some way to accomplish this with one of the transitive closure operators. My best guess is something like:
pred no_cycles {
all d: Distillate | no d & d.^(blended_from.distillate)
}
Question: How would you model this constraint?
The next one is that any Maturation in a blend should be a part of the set of Maturations that make up a Contents:
pred all_blend_components_belong_to_contents {
all c: Contents |
all m: Maturation |
m.distillate.blended_from in c.maturations
}
The last bit I want to model is that it doesn’t make sense for a distillate to be “blended” from a single Maturation i.e. Distillate.blended_from should have a cardinality of 0 or >2. This seems like something simple to model but I don’t actually know how you access the cardinality of a set in Alloy.
Question: How do you constrain the number of atoms in a signature to specific values e.g. 0 and >2?
Wrap up
That ended up being a small novel. If you read this far you’re a saint and I appreciate your help. I’m trying to learn Alloy so that I can slowly introduce it to friends and coworkers.
the help is much appreciated.