This topic has been improperly named, I should have named it "how to construct partial instances"
-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

I would like to understand better how symmetry breaking optimizations work in util/ordering to make better use of them or maybe apply it to my own state ordering structes. Is there any articles, material or even code I could read to understand that better? Motivation for concern follows:
  I'm currently involved in a project of transformation of OntoUML models to Alloy, for validation purposes.
OntoUML's meta-properties are based on modal logics and the states of the model can best be represented by Kripke structures. Daniel Jackson said on http://alloy.mit.edu/community/node/452 "Do use the Alloy ordering module. It will fire built-in symmetry breaking, which will dramatically improve performance.". Motivated by that, we assumed that if we created a main course of events ordered by util/ordering only a few branches growing from this main line (representing counter factual timelines) we could have a better performance than creating a brand new ordering structure.
  For example, take a Person Alex that has three different phases: Child, Teenager and Adult. We may show that on a first moment, Alex is a child, on the second Alex is a teenager and on the last Alex is dead (no longer an instance of the model). However, one of OntoUML's phase's meta-properties says if Adult is a phase of Person there must be (logically) a moment where Alex is an Adult.
  We don't want to restrict visualization to show these logically necessary worlds in every visualization, but we understand that such worlds have a big impact on the semantics of the model and, to improve the quality of the validation process, we would like to offer a predicate that enforces the visualization of these meta-properties. That means restricting the visualization to show every logically necessary state. In the example, showing a parallel valid state where Alex is an adult (counter factual to state 3, where Alex is dead).
  We already suppose to have better performance by using this backbone ordered by util/ordering, but we are greedy about getting even better performance if we build the kripke structure to provide such symmetry breaking optimizations.

Thanks for you attention,
Bernardo

Hi: Multi-part answer.

a) util/ordering
================

util/ordering is far more efficient than if you use a constraint
to describe a list of elements. For example, suppose you write
the following:

sig Node {
  next: lone Node,
  prev: lone Node
}

fact {
  next = ~prev
  one a: Node | no a.prev && a.*next=A
  no a: Node | a in a.^next
}

The above specifies (assuming I didn't make an Alloy modeling mistake)
that there are a set of nodes, where one of it is the head,
and every node is reachable from the head, and that there are
no cycles in the list.

Alloy will have to allocate bits to represent all possible
configurations of this graph (even though we, the user, actually
knows it is not a general graph but is really just a list),
and then generate many CNF formula to forbig the various illegal
configurations... worse yet, any formula involving the "next" field
or the "prev" field will be a formula consisting of these bits,
and therefore they will be non-constant (and thus we are limited in
how much optimization we can apply to them)

On the other hand, if you write

open util/ordering[A]
sig Node { }
run ... for exactly 7 Node

Then we recognize that you simply want a list of 7 nodes.
So, (assuming the rest of your model doesn't restrict our freedom),
we can then explicitly announce that there are 7 node atoms
Node0 through Node6, and that Node0.next is the constant node Node1,
and Node1.next is the constant node Node2, etc. etc.
That is, all these are purely constants and do not need to be solved.
There are no variables to fill out, and no constraints to satisfy.

Better yet, if there are formulas involving "next" or "prev" field,
then since "next" is a compile-time constant, we can do constant propagation
as much as possible, etc.

So the performance benefit of util/ordering (when our analyzer confirms
that the rest of your model doesn't restrict our encoding freedom)
is tremendous.

In our literature, we call this "symmetry breaking", because originally
it is possible to have NodeAlex.next=NodeBrian, and NodeBrian.next=NodeScott, etc.
And it is also possible to have NodeAlex.next=NodeScott, and NodeScott.next=NodeBrian.
The two solutions are symmetric to each other, and if your model doesn't
cause one solution to be preferable to the other (and we in fact conservatively
verify that), then we break the symmetry, and simply force NodeAlex to be the first node,
and NodeBrian to be the second node, etc. etc.

b) Partial Instance
===================

In our literature, we mean that if you already know part of the instance,
then it's better if you provide it to us directly (rather than
write constraints that we then have to solve, which takes up
valuable bits in the state space and also harms constant propagation).

For example, the following 2 models are equivalent:

model slow
abstract sig Person { age: Int, boss: set Person }
one sig A, B, C extends Person { }
fact { A.age=2  B.age=3 C.age=4 }

model fast
abstract sig Person { boss: set Person }
one sig A, B, C extends Person { }
fun age : Person->Int { A->2 + B->3 + C->4 }

In the slow model, we allocate bits for the possible age for each person.
And then write an expensive fact which rejects (at SAT solving time)
any solution which doesn't happen to assign 2 as A's age, and 3 as B's age...

In the fast model, we don't allocate any bits for the age field.
Instead, we declare a constant function (a function that doesn't take
any argument and is therefore a constant expression) which is a binary
relation from Person to Int, containing the union of 3 constant tuples
(A,2), (B,3) and (C,4).

In almost every way (except minor differences with compiler scoping),
the two models are interchangable. You can still write formulas
like "all x: Person | x.age > 0" (since in the first model, age is a field
that will be dereferenced, and in the second model, age is a constant function
that will be invoked). But with the second case, the "all x: Person | x.age > 0"
is actually evaluated at compile time into a "constant true",
without requiring the SAT solver at all.

(Arguably, the compiler should be able to "look at" the first model,
and be smarter, and turn certain bits into constants automatically.
Since there is an unlimited number of ways for humans to write the same thing,
obviously we can never detect them all. So what we can do is detect some
common patterns, and auto-optimize them.  We have started work on this,
and have a few simple patterns we look for, but we hope to improve on this front
in the near future)

c) Optimizing your specific model
=================================

Post the performance-intensive part of your model, and I and others can then comment
on whether certain parts of it can be rewritten to be more efficient.

Sincerely,
Felix Chang
Alloy4 Developer

Dear Felix,
Thanks for your (as usual) quick reply. Your remarks were very illuminating.
I have so far only dealt with the so called "backbone" of the state transitioning but a fellow NEMO member has done the transformation using the Kripke structure. So I still have to merge his solution to mine and once I am done, I'll post it here for c). Thank you very much for the offer.
The partial instance optimization will surely be used to reach for farther states, fixating initial states and pushing the heavy solving job to subsequent states.
As I am writing academic papers, I need a reference for these information. What "literature" are you referring to? Jackson's book? If articles, are they available online?
Once more,
Thank you,
Bernardo

-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

We haven't published a paper on the Alloy4 tool yet,
but we have published several papers on the underlying Kodkod engine
which discuss the importance and implementation of partial instance.

A partial instance is when part of the model is already fixed, prior to solving.

In the naive formulation, I might represent known values as constraints that happen to only have a unique solution.  However, that approach can require lots of analysis time.  The analysis is a function of the total state space, counting the parts that do not conform to the partial instance.

Alloy 4's Java API has the notion of a partial instance, wherein you can have pre-defined constant values without slowing down the analysis.  As a result, the analysis is only a function of the unconstrained portions of the state space.

You can only directly define a partial instance via the API, but you can sometimes write constraints in the textual language that will get translated into a partial instance (rather than normal constraints).  In general, you do this by using equality statements, like

relation = (alpha -> beta + beta -> gamma + gamma -> delta)

However, it can be a bit tricky to get this to work in general.  With the Java API (rather than the textual language), I hear it is quite trivial.

Hello fellow Alloy community users, long time no see :]
I'm currently writing a paper to UML+FM about my aproach to a transformation from a version of UML (namely, OntoUML) to Alloy, to function as an instance generator, as means to check if the model conforms to the conceptualization.
I've re-read the anwser felix gave me on May, and have understood diferently than I did before. It seems now to me that it is not so trivial to construct partial instances as a means to reduce solving time, as I expected.
My purpose was to be able to generate some random instance, with a few states, "lock" some atoms and their relations as constants (with the use of partial instances), thus reducing solving effort and allowing me to enlarge the scope and populate the instance...
Could this be done easily through the API? Since I wrote a transformation from the modeling language to Alloy, I could just as well write to the API language and add this feature to my tool..
 Would I get the results I'm describing?
Thank you,

----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

Also, I'm not sure how writing through the API is different from writing Alloy code... Is there anything I can read about that?
-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

Hi: I recommend first generating Alloy models, and find ways
to optimize it and improve scalability... if all else fails, then try the API.

There are several things that the API helps, but other than that
it is still the same Alloy language; there are no hidden features.
So you are more likely to make a major performance improvement
by thinking about different ways to describe or represent
your Alloy "model".  Whether you feed this conceptual Alloy "model"
into the Alloy analyzer via a text file or via a Java object graph
is likely not going to matter much.

(On the other hand, for fully automatic analysis and model generation,
you should seriously consider generating Kodkod models as a possibility.
I still think it's immensely easier to reason about and optimize
the model using the Alloy language and tool; but once you got it
down to a nice and efficient form, you can consider letting your tool
automatically generate a equivalent "Kodkod" model.
At the Kodkod level, there are a lot more tweaks and techniques
you can do to squeeze every bit of performance out of your computer)

Yes, thank you, I have indeed reached an Alloy transformation which I assume is the best possible. Would writing an equivalent kodkod model allow me to generate partial instances without altering the model? That is, in your Person-age example, would it still be possible to leave the Person signature with the age field, generate the three constants I know of (A,B and C, with 3,4,5 ages respectively), and leave the analyser to find further arbitrary instances?
My expectations are something like this:
Suppose a model with a scope of 5. The Analyser finds a valid model, I transform the state of affairs (atoms which exist and their relations) into constants and enlarge the scope to 10. Repeat this again and again, enlarging the scope to populate the model. Is this possible, and would this drastically improve the ability to enlarge scope, while keeping the processing time short?
-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

Kodkod and Alloy have the same expressiveness and operators.
For example, both can do arbitrary unary quantification,
and both have the exact same limitation regarding non-unary quantification...
since Alloy translates into Kodkod for solving.

So in terms of formulas, structures, and operations...
it's really straightforward.  If you have a binary relation
from X to Y in Alloy, you would just declare a binary relation
in Kodkod from X to Y... and so on.

Furthermore, partial instance can be specified precisely.
So you definitely can declare the 'age' relation,
and fill in whatever tuples you want to always exist in it,
and you can also further block out whatever tuples you want
to never exist in it.

*However*

Many of the higher level constructs are just syntactic sugars in Alloy.
So your question asked about Person "signature" and a "scope" of 5.
In Kodkod there are no signatures. No inheritance. No fields.
Just a flat collection of atoms, and relations that can overlap.
And there are no "scope" either.  For each unary relation
you list out exactly the atoms that must be in it, and the list
of atoms that may be in it.  So... it's quite a bit of a
mental model shift.  Please look at the kodkod webpage
and download some of the sample Java files. (Also, you can
also go to Alloy analyzer, go to Options, change SAT solver to Kodkod.
and look at the Kodkod output that is automatically generated
when you execute an Alloy model)

Well, I guess I sort of reasoned about Alloy's instance level that way already, so the mental model shift won't be that far... However, the lack of scope is a major shift! I'll look into Kodkod webpage, and do as you said! Would you also be so kind as to give me some tips on articles or references I could read to better understand how Alloy generates the arbitrary instances? It seems to me that if on the kodkod level you have to list out exactly the atoms that are in each unary relation, there must be some kind of "set of atoms generator", right? Also, that seems very odd, since for a single kodkod file, multiple instances are generated (using the "next" in the visualizer).
Again,
thank you very much,
-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)

No, kodkod doesn't fix each unary relation to a fix value; I said you tell kodkod what atoms must be in a relation, and you also tell kodkod what atoms *may* be in the relation.

Thus, one kodkod model encodes a constraint solving problem where there may be multiple solutions (just like alloy)

There are several papers by kodkod author Emina Torlak.

Thank you very much Felix, as always you have been extremely helpful. :]
Most of my Alloy inner workings, or 'advanced' knowledge is thanks to you.
-----
Bernardo F. B. Braga
Undergraduate bachelor student at Universidade Federal do Espirito Santo (UFES)
Member of the Ontology and Conceptual Modelling Research Group (NEMO)