Refactoring Alloy models

问题:

In a model I started to sketch in Alloy the other day, I get the following message when I attempt to find an instance of a particular predicate:

Translation capacity exceeded. In this scope, universe contains 34 atoms and relations of arity 12 cannot be represented. Visit http://alloy.mit.edu/ for advice on refactoring.

Any suggestions of where on the site alloy.mit.edu to look? I'm not finding anything with an obvious label like "Refactoring models that exceed translation capacity".

That's the essential question.

[Postscript: the cause of my problem appears to have been a bad initial formulation of the quantified variable declarations I was using in a predicate; the problem went away once I got the syntax of the declarations right. The full details are not instructive enough to be worth keeping on record, so I'm dropping the original description of the specifics. The short version is: to elicit the instantiation of a particular concrete example, I initially wrote a predicate of the form

    pred m {
      one t1 : table,
          r1, r2, r3 : row,
          c1, c2 : column,
          c11, c21 : headingcell, 
          c12, c22, c13, c23 : datacell | {

    ... // description of the example here

      }
    }

The one scopes all twelve variables, and is [I am told on good authority] translated internally into a set comprehension defined by a relation of arity 12. What I wanted to say was something more like the following, which does not raise the translation-capacity issue:

pred m {
   some t1 : table |
   some disj r1, r2, r3 : row |
   some disj c1, c2 : column |
   some disj c11, c21 : headingcell |
   some disj c12, c22, c13, c23 : datacell | {
     ...
   }
}

So: one way to fix some models which elicit the translation-capacity error message is to clean up the quantification of variables.

The basic question, however, retains its interest: when a model elicits the translation-capcity error message and the quantifiers are already clean and correct, is there a document to read?]

回答1:

The kind of refactoring needed in this case is unlikely to be a simple syntactic one. Rather, it here means restructuring the model so that it doesn't use a relation of that high arity. In your example above, I can't really see which relation has arity 12. If you post (or send me) a self-contained model, I can look at it, identify the problematic relation, and maybe even suggest how to avoid it.