Home Articles

重构合金模型

Asked
Viewed 1581 times
2

在模型中,我开始在Alloy中绘制草图,当我尝试查找特定谓词的实例时,我收到以下消息:

超出翻译能力 . 在此范围内,Universe包含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 范围所有十二个变量,并且[我被告知有良好的权威]内部翻译成一个由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 | {
     ...
   }
}

因此:修复一些引出转换容量错误消息的模型的一种方法是清理变量的量化 .

然而,基本问题仍然保留其兴趣:当模型引出翻译 - 容量错误消息并且量词已经清晰且正确时,是否有要阅读的文档?]

1 Answer

  • 2

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

Related