alloy - 重构合金模型

Question

在我前几天开始用 Alloy 绘制的模型中，当我尝试查找特定谓词的实例时，我收到以下消息:

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.

关于在 Alloy.mit.edu 网站上哪里可以查看有什么建议吗？我没有找到任何带有明显标签的内容，例如“重构超出翻译能力的模型”。

这是最重要的问题。

[后记:我的问题的原因似乎是我在谓词中使用的量化变量声明的初始表述不正确；一旦我正确地理解了声明的语法，问题就消失了。完整的细节没有足够的启发性，不值得记录下来，所以我放弃了细节的原始描述。简短的版本是:为了引出特定具体示例的实例化，我最初编写了以下形式的谓词

    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

      }
    }

one 涵盖所有 12 个变量，并且[据权威人士告知]在内部翻译为由 arity 12 关系定义的集合理解。我想说的是类似于以下内容，不会引发翻译能力问题:

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 | {
     ...
   }
}

因此:修复某些引发翻译能力错误消息的模型的一种方法是清理变量的量化。

但是，基本问题仍然很有趣:当模型引发翻译能力错误消息并且量词已经干净且正确时，是否有文档可供阅读？]

Answer 1

这种情况下所需的重构不太可能是简单的语法重构。相反，它在这里意味着重构模型，以便它不使用如此高数量的关系。在上面的示例中，我无法真正看出哪个关系的数量为 12。如果您发布(或发送给我)一个独立的模型，我可以查看它，识别有问题的关系，甚至可能建议如何避免它。