如何在合金分析仪中对两个以上的数字求和？

Question

我正在尝试将合金中一组中的所有数字相加。 例如，在签名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。

Answer 1

Alloy 具有内置

sum

功能，所以只需执行

sum[value]

即可。

Answer 2

正如这个答案中提到的，合金有一个可以使用的

sum

关键字（与

sum

函数不同）。

一般格式为：

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

变量信号值

这里有一个简单的例子，将餐厅一日三餐的销售数量相加。特别要注意

sum

中

fun sum_sales

关键字的使用。

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

关联的值保持不变，但允许

Meal

的数量变化。您可以使用将每种餐食类型映射到销售数量的关系来对此进行建模，如下所示。

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 }

Answer 3

我认为 Alloy 中不允许递归。但是，可以通过 Alloy 的库

Int

累积

util/ordering

值。

open util/ordering[abc]

abstract sig abc {
  ,value : Int
  ,accumulatedValue : Int
}{
  accumulatedValue = this.prev.@accumulatedValue fun/add value
}

one sig a,b,c extends abc {}

assert equivalence {
  last.accumulatedValue = ( (a.value fun/add b.value)  fun/add c.value )
}

check equivalence

注释，

• util/ordering

  对参数化签名进行排序。

• fun/add

  是一个内置函数，实现两个整数的二进制加法。

• 在隐式事实或签名事实（即作为签名一部分的事实）中，您可以使用

  @

  运算符访问原始关系。

您可以用其他方式编写代码。

open util/ordering[abc]
open util/integer

abstract sig abc {
  ,value : Int
  ,accumulatedValue : Int
}

one sig a,b,c extends abc {}

fact {
  all element : abc | element.accumulatedValue = integer/add[ element.(ordering/prev).accumulatedValue , element.value ]
}

assert equivalence {
  (ordering/last).accumulatedValue =  integer/add[ ( integer/add[ a.value , b.value ] ) , c.value ]
}

check equivalence