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

Question

我正在尝试查看是否可以让 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)
}

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

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

score 3 · Accepted Answer

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

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

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

1 回答 1