让合金找到特定集合的最大答案答案

【问题标题】：Getting Alloy to find the largest answer for particular sets让合金找到特定集合的最大答案
【发布时间】：2012-09-02 13:58:49
【问题描述】：

我正在尝试让 Alloy 返回特定集合的最大可能答案。因此，在本例中，我希望模型查找器不生成答案 x={}、x=A 和 x=B。

abstract sig X{}
one sig A extends X{}
one sig B extends X{}

pred(x: set X) {
  x in A + B 
}

我已经尝试了一些类似的东西：

pred(x: set X) {
    x in A + B and 
    no y : set X |
        y in A + B and #(y) > #(x)
}

但我得到一个错误，即无法进行分析，因为它需要更高阶的量化。

我想知道是否有可能（或更简单）的方法来做到这一点？

【问题讨论】：

标签： alloy

【解决方案1】：

Alloy 目前没有任何内置功能来生成最大或最小的解决方案。是的，你说得对，指定一个解决方案是最大的通常需要更高阶的量化。但是，您可以通过一阶量化确保解至少是局部最大值：

    pred p (x: set X) {...}

    pred locally_maximal_p (x: set X) {
      p(x)
      no e: X - x | p(x + e)
      }

【讨论】：