重构合金模型

Question

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

已超出翻译容量。 在这个范围内，宇宙包含 34 个原子 并且无法表示 arity 12 的关系。 请访问 http://alloy.mit.edu/ 获取有关重构的建议。

有什么建议可以在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。如果你发布（或发送给我）一个独立的模型，我可以查看它，找出有问题的关系，甚至可能建议如何避免它.