Search code examples
alloy

Sum of nested values in Alloy

I'm starting with definitions similar to these below

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

I'd like an expression that can produce the sum of all values contained inside something of type Top. Top when written as a nested set, would be something like {{3, 4}, {7}}. The result of the nested sum in this case should be 14.

This function of course just gives the number of elements in the outer set.

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

I believe I need to use the built-in sum function and a set comprehension, but Alloy syntax is still somewhat arcane to me.

Solution

  • For this, you need a nested sum expression:

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

    The general format is:

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