How to sum more than two numbers in Alloy Analyzer?

Question

I am trying to sum all the numbers in a set in Alloy. For instance, in the signature abc, I want the value to be the sum of a.value + b.value + c.value, which is 4+1+3=8.

However, if I use "+", it gives me the union set and not the sum.

PS. I know there is the "plus" (as I used it in sig sumab), but this only allows me to sum two values.

Thanks

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

Note: I wrote this in pseudo-code, it may help to get to an answer:

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}]]
}

Note 2. The function sum may seem to be a good idea, but if I sum 1+1+1=1, the result will be 1 intead of 3 as the only number in the set is 1.

Answer 1

Alloy comes with a built-in sum function, so just do sum[value].

Answer 2

As mentioned in this answer, Alloy has a sum keyword (different than the sum function) which can be used.

The general format is:

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

Variable sig values

Here's a simple example that sums the number of sales during a day for a restaurant's three meals. In particular, note the use of the sum keyword in 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 }

This works even when all meals have the same number of sales (1 + 1 + 1 = 3), as shown in this check.

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

Here are some other ways to play around with the example.

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 }

Constant sig values

Another way you might want to use this is to have the value associated with each type of Meal be constant, but allow the number of Meals to vary. You can model this with a relation mapping each meal type to a number of sales as follows.

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 }