.

Route.cfg

+SPECIFICATION
+Spec
+
+INVARIANT
+TypeOK
+Inv
+Terminated_then_PathsOK
+
+PROPERTY
+Eventually_Terminated
+
+CONSTANT NoRoute = NoRoute
+CONSTANT Inf = Inf
+
+\* --------
+
+CONSTANTS
+r = r
+n1 = n1
+n2 = n2
+
+CONSTANT root = r
+CONSTANT Nodes = {r, n1, n2}
+CONSTANT Edges = {{r,n1}, {n1,n2}}

Route.tla

+(*
+-------- CONFIG Route ---------
+
+CONSTANT NoRoute = ZZZNoRoute
+CONSTANT Inf = ZZZInf
+
+=================
+*)
+
 ------------------------------- MODULE Route -------------------------------
 EXTENDS Integers, FiniteSets, Sequences
 
@@ -236,4 +245,10 @@ SumSet(S) == IF S = {}  THEN 0
                             IN y + SumSet(S \ {y})
 
 
+
+------
+
+Eventually_Terminated   == <>Terminated
+Terminated_then_PathsOK == Terminated => PathsOK
+
 =============================================================================