【问题标题】：How to sum more than two numbers in Alloy Analyzer?如何在合金分析仪中对两个以上的数字求和？
【发布时间】：2021-09-06 16:16:02
【问题描述】：

我正在尝试对 Alloy 中的一组数字求和。例如，在签名 abc 中，我希望值为 a.value + b.value + c.value 之和，即 4+1+3=8。

但是，如果我使用 "+"，它会给我联合集而不是总和。

PS。我知道有 "plus"（就像我在 sig sumab 中使用的那样），但这只允许我将两个值相加。

谢谢

open util/integer

sig a{value: Int}
{
value = 4
}
sig b{value: Int}
{
value = 1
}
sig c{value: Int}
{
value = 3
}
sig abc{value: set Int}
{
    value = a.value + b.value + c.value
}

sig sumab{
    value : Int
}
{
value = plus[a.value, b.value]
}

pred add{}

run add for 4 int, exactly 1 sumab, exactly 1 a, exactly 1 b, exactly 1 c, exactly 1 abc

注意：我是用伪代码写的，可能有助于得到答案：

fun plusN [setInt : set de Int] : Int {  // function "plusN" should take a set of integers "setInt", return an integer
    if #setInt = 2  //if only two numbers in set, sum them
            then plus[max setInt , min setInt]
    else // if more than 2, use recursion
            plusN [max setInt  , plusN[{setInt - max setInt}]]
}

注意 2。函数 sum 似乎是个好主意，但如果我将 1+1+1=1 相加，结果将是 1 而不是 3 作为唯一的数字设置为 1。

【问题讨论】：

为什么要对集合中的值求和？如果你能给我们一些你想要完成的事情的背景，它可能会帮助我们建议一种对你有用的技术。
我有一组任务，每个任务都有不同的成本；以及它们可以处理的具有最大成本的一组处理单元。对于每个生成的模型，我将分配给每个处理单元的任务成本求和，以使其不超过其容量。谢谢。
好的——那么您确定 Alloy 是解决您问题的正确工具吗？
好吧，我可以将任务分配给处理单元。我的问题是当我尝试在带宽之间获取每个处理单元的任务成本总和时。谢谢。
我的意思是，你正在解决的问题（如果我理解正确的话）看起来有点具体——一点也不抽象。因此，我想知道 Alloy 是否适合您的目的。

标签： alloy model-checking

【解决方案1】：

Alloy 带有内置的sum 功能，所以只需使用sum[value]。

【讨论】：

我再次尝试使用我的实际应用程序，但没有成功。如果数字不同 sum[{1,2,3}]=6，则有效，但相同时无效，例如： a.value= 1 , b.value= 1 和 c.value= 1, sum [a.value, b.value, c.value]=1，因为集合只包含 1。
这就是我所做的：``` sig a{value: set Int} { value = {int 1 + int 2 + int 3} } sig suma{ value : Int } {value = sum [a.value] } pred add{} run add for 5 int, 正好 1 suma, 正好 1 a```
如果由于集合中的每个元素都是唯一的而不能将相同的值两次传递给 sum 函数，则可以强制每个值整数是不相交的。它很脏，但它会让你的模型工作。如果你需要证明使用 disjoint 的合理性，你可以说这是因为前面提到的合金限制
你能告诉我怎么做吗？如果我创建类似：fact{disj [a.value,b.value]}，其中 a.value 和 b.value 是相同的 int，则找不到模型（可以理解）。

【解决方案2】：

正如this answer 中提到的，Alloy 有一个可以使用的sum 关键字（不同于sum 函数）。

一般格式为：

sum e: <set> | <expression involving e>

变量 sig 值

下面是一个简单的示例，它汇总了餐厅三餐在一天中的销售额。特别要注意fun sum_sales 中sum 关键字的使用。

one sig Restaurant { total_sales: Int }
abstract sig Meal { sales: Int }
one sig Breakfast, Lunch, Dinner in Meal {}

// Each meal only falls in one category
fact { disj[Breakfast, Lunch, Dinner] }
// Every meal is in some category
fact { Breakfast + Lunch + Dinner = Meal }

// Keep the numbers small because the max alloy int is 7
fact { all m: Meal | m.sales <= 4 }
// Negative sales don't make sense
fact { all m: Meal | m.sales >= 0 }

fun sum_sales: Int { sum m: Meal | m.sales }
fact { Restaurant.total_sales = sum_sales }

即使所有餐点的销售额相同 (1 + 1 + 1 = 3)，此方法也有效，如 check 所示。

check { (all m: Meal | m.sales = 1) => Restaurant.total_sales = 3 }

这里有一些其他的方法来玩这个例子。

check {
    {
        // One meal with three sales
        #{ m: Meal | m.sales = 3 } = 1
        // Two meals with one sale
        #{ m: Meal | m.sales = 1 } = 2
    } => Restaurant.total_sales = 5
}

run { Restaurant.total_sales = 5 }

恒定信号值

您可能希望使用它的另一种方法是让与Meal 的每种类型关联的值保持不变，但允许Meals 的数量变化。您可以使用将每种膳食类型映射到多个销售额的关系来对此进行建模，如下所示。

one sig Restaurant { total_sales: Int }
abstract sig Meal {}
lone sig Breakfast, Lunch, Dinner in Meal {}

// Each meal only falls in one category
fact { disj[Breakfast, Lunch, Dinner] }
// Every meal is in some category
fact { Breakfast + Lunch + Dinner = Meal }

fun meal_sales: Meal -> Int {
    Breakfast -> 2
    + Lunch -> 2
    + Dinner -> 3
}

fun sum_sales: Int { sum m: Meal | m.meal_sales }
fact { Restaurant.total_sales = sum_sales }

check { #Meal = 3 => Restaurant.total_sales = 6 }
run { Restaurant.total_sales = 5 }

【讨论】：