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>