How to find the sum of a set of functions in TLA+?

Question

Let's say I have a set of functions

MySet == ("A" :> 15 @@ "B" :> 20 @@ "C" :> 32)

I want to get X == 15 + 20 + 32, how can I do this in TLA+? Thank you.

Answer 1

EXTENDS Functions

Sum == FoldFunction(+, 0, MySet)

https://github.com/tlaplus/CommunityModules/blob/master/modules/Functions.tla#L112-L124

Answer 2

Sorry for the late answer, in the end here is how I did it.

Assuming we have the set of inputs:

MyInputs == {"A", "B", "C"}
MyFunctions == ("A" :> 15 @@ "B" :> 20 @@ "C" :> 32)

RECURSIVE Accumulate(_, _, _)
Accumulate(val, inputs, funcs) ==
    IF inputs = {}
    THEN val
    ELSE
        LET x == CHOOSE y \in inputs : TRUE
        IN Accumulate(val + funcs[x], inputs \ {x}, funcs)

sum == Accumulate(0, MyInputs, MyFunctions)