.

Route.tla

 ------------------------------- MODULE Route -------------------------------
-EXTENDS FiniteSets
+EXTENDS Integers, FiniteSets, Sequences
 
 CONSTANT Nodes, Edges, root
 
@@ -22,4 +22,21 @@ Connected(i,j) ==
 ASSUME \A i,j \in Nodes : Connected(i,j)
 
 
+
+
+
+--------
+
+RECURSIVE SumSeq(_)
+SumSeq(S) == IF S = << >>  THEN 0
+                           ELSE Head(S) + SumSeq(Tail(S))
+
+
+RECURSIVE SumSet(_)
+SumSet(S) == IF S = {}  THEN 0
+                        ELSE
+                            LET y == CHOOSE x \in S : TRUE
+                            IN y + SumSet(S \ {y})
+
+
 =============================================================================