From d7f4d2d73284a41c93dd601f6cbbdf3c7148854f Mon Sep 17 00:00:00 2001
From: Sergiu Ivanov <sivanov@colimite.fr>
Date: Thu, 15 Sep 2022 00:57:38 +0200
Subject: [PATCH] Implement build-state-graph*/annotated.

---
 dynamics.rkt | 29 ++++++++++++++++++++++++++++-
 networks.rkt |  6 ++++++
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/dynamics.rkt b/dynamics.rkt
index f50e70b..d40bcab 100644
--- a/dynamics.rkt
+++ b/dynamics.rkt
@@ -33,5 +33,32 @@
     (define/abstract/error (build-state-graph* sts nsteps))
 
     (: build-state-graph*/annotated (-> (Listof State) (U Integer 'full) Graph))
-    (define/abstract/error (build-state-graph*/annotated nsteps sts))
+    ;; TODO: Integer -> Positive-Integer
+    (define/public (build-state-graph*/annotated sts nsteps)
+      (define (all-steps-done? k)
+        (if (equal? nsteps 'full)
+            #f ; keep going forever
+            (>= (assert-type k Integer) nsteps)))
+      (weighted-graph/directed
+       (let build-graph : (Listof (List Modality State State))
+            ([visited-states : (Setof State) (set)]
+             [states : (Setof State) (list->set sts)]
+             [edges : (Listof (List Modality State State)) '()]
+             [k 1])
+         (define new-edges
+           (for*/list : (Listof (List Modality State State))
+                      ([s (in-set states)] ; the state we are looking at
+                       [out (in-list (step/annotated s))]) ; the arrows going out of s
+             (list (car out) s (cdr out))))
+         (define edges/full (append edges new-edges))
+         (define new-states
+           (list->set (map (inst caddr Modality State State) new-edges)))
+         (define new-states-pruned
+           (set-subtract new-states visited-states))
+         (if (or (set-empty? new-states-pruned) (all-steps-done? k))
+             edges/full
+             (build-graph (set-union visited-states new-states-pruned)
+                          new-states-pruned
+                          edges/full
+                          (add1 k))))))
     ))
diff --git a/networks.rkt b/networks.rkt
index 13fdc80..cb8ce2a 100644
--- a/networks.rkt
+++ b/networks.rkt
@@ -561,6 +561,12 @@
         (check-equal? (list->set (send dyn-asyn step* (list s1 s2)))
                       (list->set (append (send dyn-asyn step s1)
                                          (send dyn-asyn step s2)))))
+      (test-case "dynamics%:build-state-graph*/annotated"
+        (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 2))
+                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"'(x y z)\"];\n\t\tnode2 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
+        (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 'full))
+                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [label=\"'(x y z)\"];\n\t\tnode1 -> node3 [label=\"'(x y z)\"];\n\t\tnode2 -> node1 [label=\"'(x y z)\"];\n\t\tnode3 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
+        )
       )
     )
   )