合金是否可以最大限度地降低成本？答案

【问题标题】：Is cost minimization possible in Alloy?合金是否可以最大限度地降低成本？
【发布时间】：2013-09-02 18:24:51
【问题描述】：

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。

如果可能的话怎么用Alloy写这个东西？

非常感谢您的热情回复。

【问题讨论】：

标签： alloy

【解决方案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

但如果你尝试运行它，你会得到以下错误：

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

你可以做的是检查是否存在一组总价格低于给定价格的物品，例如，

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 以得出相同的结论。

【讨论】：

"但是你可以迭代地运行Alloy来得出相同的结论" ------- 是否可以自动进行这个迭代？还是我需要手动多次运行命令才能得到答案？
不在 Alloy Analyzer GUI 中，但您可以使用 Alloy Java API 编写一个小型 Java 程序来自动化整个过程。