1 
abstract sig Item {
    price: one Int
}

one sig item1 extends Item {} { 
    price = 1
}

one sig item2 extends Item {} { 
    price = 2
}

one sig item3 extends Item {} { 
    price = 3
}

one sig item4 extends Item {} { 
    price = 4
}

// .. 同样的方式项目 4 到 10

是否可以选择 n 个（使得 n = 1 到 10）个项目，以使所选项目的价格总和最小？

对于 n=3 个项目，结果应该是 item1、item2 和 item3。

如果可能的话如何用合金写这个东西？

非常感谢您的友好回复。

4

1 回答 1

1

可以编写这样一个高阶查询（例如，为我找到一组商品，使得没有其他商品的总价更低），但无法自动解决它。不过有一些解决方法。

首先，这是重写模型的方法，这样您就不必为从 1 到 10 的价格手动编写 10 个不同的信号：

sig Item {
  price: one Int
}

pred nItems[n: Int] {
  #Item = n
  all i: Int | (1 <= i && i <= n) => one price.i
}

fact { nItems[10] }

现在，您可以像这样在 Alloy 中表达上述查询：

fun isum[iset: set Item]: Int {
  sum item: iset | item.price
}

run {
  some miniset: set Item | 
    #miniset = 3 and
    no iset: set Item | 
      #iset = #miniset and
      isum[iset] < isum[miniset]
} for 10 but 5 Int

但是如果您尝试运行它，您将收到以下错误：

无法进行分析，因为它需要无法进行 sklemized 的高阶量化。

相反，您可以做的是检查是否存在一组总价格低于给定价格的项目，例如，

pred lowerThan[iset: set Item, num: Int, min: Int] {
  #iset = num and
  isum[iset] < min
} 

check {
  no iset: set Item |
   iset.lowerThan[3, 7]
} for 10 but 5 Int

在此示例中，要检查的属性是不存在总价小于 7 的正好 3 个项目的集合。如果你现在让 Alloy 检查这个属性，你会得到一个反例，其中iset正好包含 3 个最低价格的项目，因此它的总价格是 6。然后如果你改变上面的检查命令来询问是否有一个集合在总价低于 6 的 3 件商品中，您不会得到反例，这意味着 6 确实是可能的最低价格。如您所见，您不能要求 Alloy 在一次运行中告诉您答案是 6，但您可以反复运行 Alloy 以得出相同的结论。

于 2013-09-02T21:43:25.233 回答