# A tip for working with complex models **URL:** \ **Category:** models\ **Created:** [September 18, 2020, 4:32pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100 "2020-09-18T16:32:48Z")\ **Posts on this page:** 18\ **Page:** 1
**Author:** ![pamela](https://avatars.discourse-cdn.com/v4/letter/p/a88e4f/32.png) [@pamela](https://alloytools.discourse.group/u/pamela)\ **Post date:** [September 18, 2020, 4:32pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/1 "2020-09-18T16:32:48Z")
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! ---
**Author:** ![peter](https://avatars.discourse-cdn.com/v4/letter/p/278dde/32.png) [@peter](https://alloytools.discourse.group/u/peter)\ **Post date:** [September 18, 2020, 5:22pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/2 "2020-09-18T17:22:18Z")
You considered using enums for this? ---
**Author:** ![pamela](https://avatars.discourse-cdn.com/v4/letter/p/a88e4f/32.png) [@pamela](https://alloytools.discourse.group/u/pamela)\ **Post date:** [September 18, 2020, 5:38pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/3 "2020-09-18T17:38:02Z")
What’s an enum? If it’s not in the index to Daniel’s book, I have no way to know about it. ---
**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\ **Post date:** [September 18, 2020, 7:54pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/4 "2020-09-18T19:54:35Z")
Enum is new since the orange book. Instead of ``` abstract sig Node{} one sig N0, N1, N2 extends Node {} ``` write `enum Node {N0, N1, N2}` ---
**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\ **Post date:** [September 18, 2020, 8:02pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/5 "2020-09-18T20:02:40Z")
I was just about to post the same tip! I like it better than enums because 1. Enums don’t let you add fields 2. Enums implicitly import `ordering`, which makes `first` ambiguous. Also, you can write `lone N1, N2 ...` to make them optional, which is sometimes real useful. You also don’t need to write `some n1: N1 ... | p[n1]`, as you can just write `p[N1]`. ---
**Author:** ![pamela](https://avatars.discourse-cdn.com/v4/letter/p/a88e4f/32.png) [@pamela](https://alloytools.discourse.group/u/pamela)\ **Post date:** [September 18, 2020, 8:59pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/6 "2020-09-18T20:59:59Z")
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. ---
**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\ **Post date:** [September 18, 2020, 9:17pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/7 "2020-09-18T21:17:24Z")
Working on it! Here’s what I have for enums: [https://alloy.readthedocs.io/en/latest/language/signatures.html?highlight=enum#enums](https://alloy.readthedocs.io/en/latest/language/signatures.html?highlight=enum#enums) ---
**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\ **Post date:** [September 19, 2020, 5:00pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/8 "2020-09-19T17:00:04Z")
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. ---
**Author:** ![peter](https://avatars.discourse-cdn.com/v4/letter/p/278dde/32.png) [@peter](https://alloytools.discourse.group/u/peter)\ **Post date:** [September 19, 2020, 8:03pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/9 "2020-09-19T20:03:12Z")
I really love them but I’m a sucker for concisenesd. Less is more. ---
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [September 20, 2020, 8:12am UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/10 "2020-09-20T08:12:31Z")
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: ```auto abstract sig Node{} one sig N0, N1, N2 extends Node {} ``` you just keep the signature `Node` and write your command as: ```auto 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? ---
**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\ **Post date:** [September 21, 2020, 8:13am UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/11 "2020-09-21T08:13:07Z")
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. ---
**Author:** ![pamela](https://avatars.discourse-cdn.com/v4/letter/p/a88e4f/32.png) [@pamela](https://alloytools.discourse.group/u/pamela)\ **Post date:** [September 21, 2020, 2:25pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/12 "2020-09-21T14:25:28Z")
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? ---
**Author:** ![tim](https://avatars.discourse-cdn.com/v4/letter/t/ce73a5/32.png) [@tim](https://alloytools.discourse.group/u/tim)\ **Post date:** [September 21, 2020, 2:37pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/13 "2020-09-21T14:37:19Z")
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?) cheers, – Tim ---
**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\ **Post date:** [September 21, 2020, 2:44pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/14 "2020-09-21T14:44:11Z")
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. ---
**Author:** ![pamela](https://avatars.discourse-cdn.com/v4/letter/p/a88e4f/32.png) [@pamela](https://alloytools.discourse.group/u/pamela)\ **Post date:** [September 21, 2020, 2:51pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/15 "2020-09-21T14:51:34Z")
Be careful what you wish for! 🙂 Sending. ---
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [September 21, 2020, 7:37pm UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/16 "2020-09-21T19:37:23Z")
Absolutely, this is why I supposed it doesn’t necessarily make sense for the case Pamela described. It could be worth doing some benchmarks actually, comparing both approaches. Ditto for quantification avoidance (and I think you earned the right to make a specific post about this kind of tips 😁 ). ---
**Author:** ![nmacedo](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/nmacedo/32/74_2.png) [@nmacedo](https://alloytools.discourse.group/u/nmacedo)\ **Post date:** [September 22, 2020, 8:16am UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/17 "2020-09-22T08:16:32Z")
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. ---
**Author:** ![tim](https://avatars.discourse-cdn.com/v4/letter/t/ce73a5/32.png) [@tim](https://alloytools.discourse.group/u/tim)\ **Post date:** [September 22, 2020, 11:33am UTC](https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models/100/18 "2020-09-22T11:33:24Z")
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.