.

Route_tlc_allgraphs.py

@@ -3,6 +3,7 @@
 
 from __future__ import print_function
 import sys
+from subprocess import check_call
 
 
 class Graph:
@@ -77,6 +78,42 @@ def genGraphs(N):
 
         Sprevedges = Sedges
 
+# verify Route.tla on graph G.
+_cfg_base = """
+SPECIFICATION
+Spec
+
+INVARIANT
+TypeOK
+Inv
+Terminated_then_PathsOK
+
+PROPERTY
+Eventually_Terminated
+
+CONSTANT NoRoute = NoRoute
+CONSTANT Inf = Inf
+"""
+def TLCRoute(G):
+    cfg = _cfg_base
+    cfg += "\n\n\nCONSTANTS\n"
+    for n in G.nodes:
+        cfg += "%s = %s\n" % (n, n)
+    cfg += "\n"
+    cfg += "CONSTANT root = r\n"
+    cfg += "CONSTANT Nodes = %s\n" % setstr(G.nodes)
+    cfg += "CONSTANT Edges = %s\n" % setstr(G.edges)
+
+    writefile("Route.cfg", cfg)
+
+    check_call("./tlc", "Route.tla")
+
+
+
+
+def writefile(path, data):
+    with open(path, "w") as f:
+        f.write(data)
 
 
 
@@ -84,6 +121,7 @@ def main():
     N = int(sys.argv[1])
     for g in genGraphs(N):
         print(g)
+        TLCRoute(g)