I got this tip from Tim Nelson, and it has helped me immensely in working with very complex models of networks. Here’s a simple example.
I’m exploring a complex network function, so I want to instantiate it in a network topology I have chosen for the purpose. I have a handmade drawing with numbered nodes. But in the instance, Alloy has chosen a different numbering, and it is a huge (and error-prone) task for me to translate between the two so I can see what is going on in the instance.
The solution is singleton types N0, N1, N2, etc., which are subtypes of Node. The predicates start:
some n0: N0, n1: N1, n2: N2 . . . |
Now the node instantiating my variable n1 is N1$0, which is easy to match with my drawing.
I can’t use the visualizer because my models are complex in every dimension, and the slightest randomness in graph placement makes instances too difficult to understand. Students won’t encounter this. Thank you, Tim!
Thanks, all. This is a perfect example of the kind of documentation we need on this site. There is documentation of new features in Alloy 4, but nothing since then, and it does not include enum.
Yeah, not a fan of enum. Daniel says that they were put in at the request of his students. I can see why they’d have wanted it. But after trying them for a bit I’ve gone back to preferring the older idiom.
I seem to recall that @alcino and @nmacedo suggest, when instances are in fact arbitrary (I’m not sure it applies to @pamela’s case), to favor a disjoint existential quantification over instantiation through (l)one sigs. That is, instead of:
abstract sig Node{}
one sig N0, N1, N2 extends Node {}
you just keep the signature Node and write your command as:
run { some disj N0, N1, N2: Node | ... }
This way, due to instances not being “hard-wired” in your model, symmetry breaking will be far more effective. Is that indeed the idea, @alcino?
Yes, that is my favourite way to describe concrete scenarios, because I can have several of them in different predicates, and also works fine with symmetry breaking.
Sorry, I don’t understand how this is different from the original problem. N0 is just a variable, and it can be instantiated by Node$4, while N1 is instantiated by Node$0. What am I missing?
My (possibly deranged :-)) perspective is that adding “one” or “lone” subsigs is a sort of heavy-handed manual symmetry breaking.
I’m not arguing against the disjoint-some approach, but it’s worth noting that the change isn’t “free”. These new existentials have to be handled somehow, either by skolemization or expansion.
Current Alloy will always Skolemize top-level existentials since (I believe?) the menu doesn’t allow setting Skolem depth = -1.
In this example, Skolemizing will introduce 3 new $kolem relations: $pred_N1, $pred_N2, and $pred_N3 (where “pred” is the name of the predicate the quantifiers reside in). These increase the size of the overall search space, meaning that we now rely more on symmetry breaking than we did before. This isn’t necessarily bad, but it’s not clear to me that the disjoint-some solution is always best.
I’d ask:
(A) Am I in a world where node identities should have important semantic meaning (e.g., N1 represents Boston and N2 represents Mumbai, etc.)?
If so, giving names to the specific nodes might make sense: maybe a road from Boston to Mumbai should not be “equivalent” to a road from Mumbai to London just because the unlabeled graphs are isomorphic.
(B) Exactly why do I need these names? Can I manage with fewer? If so, that’s likely to improve efficiency overall. Example: changing “some x : Node | some n.edges” to “some edges” will avoid Skolemization into $x.
(Is anybody aware of a way to selectively avoid Skolemizing some quantifiers?)
This is really interesting. Most of all I’d like to see if we can develop a better visualizer. Can you share an example of a model and a counterexample that we can play with in the visualizer, ideally with some hints for what the viz should show? A student of mine is working on visualizing techniques and it would be great to have this as a target.
I don’t think it’s just a matter of performance. Unless these atoms have a particular semantic meaning as @tim said, using signatures forces the existence of additional atoms for every command of the model, which leads to the cumbersome task of commenting/uncommenting those sigs for each particular command (and sooner or later you’re making a mistake, I’ve been there). The some-disj pattern keeps this process local to the commands.
Agree with @nmacedo’s comment – it’s not just performance (although it can be a very visible issue) but also a language-design challenge. Alloy isn’t great at modularity when it comes to sigs or bounds. Before I posted above, I spent some time experimenting in Alloy, and had to keep commenting/uncommenting the 3 subsigs as I tried different cases. Maybe what I should have done is create 3 different modules: one with the base sig, and one specialized to each of the run commands. Unsure how that’d scale if I want to select between lots of different aspects of a larger model. (Partial instances as bounds can help a bit with this, since they can be limited in scope and built up gradually. I use them in my class, but I don’t believe base Alloy supports these.)
I just wrote up more about Skolemization, but realized I’m taking this a bit off-topic (sorry!) Will make a separate post.
Sending.
).