1

特定のセットに対して可能な限り最大の回答を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)
}

しかし、高次の定量化が必要なため、分析が不可能であるというエラーが発生します。

これを行うための可能な（またはより簡単な）方法があるかどうか疑問に思いましたか？

4

1 に答える 1

3

Alloyには現在、最大または最小のソリューションを生成するための組み込み機能がありません。もちろん、解が最大であることを指定するには、通常、より高次の定量化が必要です。ただし、一次定量化により、解が少なくとも局所的に最大になるようにすることができます。

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

    pred locally_maximal_p (x: set X) {
      p(x)
      no e: X - x | p(x + e)
      }
于 2012-09-03T21:18:59.340 に答える