Сумма вложенных значений в Alloy

Question

Я начинаю с определений, подобных приведенным ниже

sig Sub { vals : set Int }
sig Top { subs : set Sub }

Мне бы хотелось выражение, которое может вывести сумму всех значений, содержащихся внутри чего-то типа Top.Top при записи в виде вложенного набора будет выглядеть примерно так: {{3, 4}, {7}}.Результат вложенной суммы в этом случае должен быть 14.

Эта функция, конечно, просто дает количество элементов во внешнем наборе.

fun allsum[t: Top] : one Int { #t }

Я считаю, что мне нужно использоватьвстроенная функция sum и понимание набора, но синтаксис Alloy для меня все еще немного загадочен.

Answer 1

Для этого вам нужно выражение для вложенной суммы:

fun allsum[t: Top] : Int { 
    sum s: t.subs | (sum v: s.vals | v)
}

Общий формат:

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