Search code examples
tla+

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

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.

Solution 
  • EXTENDS Functions

Sum == FoldFunction(+, 0, MySet)

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