如何在Alloy Analyzer中实现两个以上数值的求和？

核心问题说明 #

• Alloy 中+运算符默认执行集合求并逻辑，并非数值加法运算
• 内置sum函数如果直接作用于Int集合，会先对集合元素去重再求和，因此1+1+1的场景会返回1，无法满足重复值累加需求
• 内置plus函数仅支持两个数值入参，无法直接完成多值累加

最优解决方案（无需自定义函数） #

如果你需要累加某一类签名所有实例的value值，直接使用带遍历的sum语法即可，该语法不会对值做去重处理：

value = sum s: (a + b + c) | s.value

你给出的示例代码修改后可直接运行得到正确结果：

open util/integer

sig a{value: Int}
{
value = 4
}
sig b{value: Int}
{
value = 1
}
sig c{value: Int}
{
value = 3
}
sig abc{value: Int}
{
    // 遍历每个实例取value累加，不会去重
    value = sum s: (a + b + c) | s.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

运行后abc.value的值即为预期的8。

通用多值累加自定义函数 #

如果需要对任意一组可重复的数值做累加，可以基于序列实现递归求和函数（序列天然支持重复元素，不会触发去重逻辑）：

// 入参为Int序列，返回所有元素的累加和
fun plusN[ints: seq Int]: Int {
  #ints = 0 => 0
  else #ints = 1 => ints[0]
  else plus[ints.last, plusN[ints.butlast]]
}

// 调用示例：计算4、1、3的和
fun testPlusN: Int {
  plusN[4->1 + 1->1 + 2->3]
}

如果你坚持使用集合作为入参，需注意集合本身的去重特性，仅适用于元素不重复的求和场景，对应实现如下：

fun plusN[setInt: set Int]: Int {
  #setInt = 0 => 0
  else #setInt = 1 => max[setInt]
  else plus[max[setInt], plusN[setInt - max[setInt]]]
}

内容的提问来源于stack exchange，提问作者Griselle Z