From b5fef760c569b87c254abd1a9bce74fde0b181ee Mon Sep 17 00:00:00 2001
From: Sergiu Ivanov <sivanov@colimite.fr>
Date: Thu, 22 Sep 2022 01:22:11 +0200
Subject: [PATCH] Type build-full-state-graph/annotated.

---
 networks.rkt               | 13 ++++++++++++-
 scribblings/networks.scrbl | 17 +++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/networks.rkt b/networks.rkt
index de827de..ab24574 100644
--- a/networks.rkt
+++ b/networks.rkt
@@ -35,6 +35,7 @@
 
    Modality Mode dynamics% Dynamics% make-syn make-asyn
    make-asyn-dynamics make-syn-dynamics build-full-state-graph
+   build-full-state-graph/annotated
    pretty-print-state pretty-print-state/01 pretty-print-state-graph-with
    pretty-print-state-graph ppsg pretty-print-state-graph/01 ppsg01
    )
@@ -708,16 +709,26 @@
           build-state-graph
           (build-all-states (network-domains (get-field network dyn)))))
 
+  (: build-full-state-graph/annotated (All (a) (-> (Dynamics% a) Graph)))
+  (define (build-full-state-graph/annotated dyn)
+    (send dyn
+          build-state-graph/annotated
+          (build-all-states (network-domains (get-field network dyn)))))
+
   (module+ test
     (let* ([n1 : (Network Boolean)
                (forms->boolean-network (hash 'x '(not y)
                                              'y 'x
                                              'z '(and y z)))]
            [dyn-syn (make-syn-dynamics n1)]
-           [sg ((inst build-full-state-graph Boolean) dyn-syn)])
+           [sg ((inst build-full-state-graph Boolean) dyn-syn)]
+           [sg/an ((inst build-full-state-graph/annotated Boolean) dyn-syn)])
       (test-case "build-full-state-graph"
         (check-equal? (graphviz sg)
                       "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode7 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [];\n\t\tnode1 -> node7 [];\n\t\tnode2 -> node4 [];\n\t\tnode3 -> node7 [];\n\t\tnode4 -> node1 [];\n\t\tnode5 -> node1 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node6 [];\n\t}\n}\n"))
+      (test-case "build-full-state-graph/annotated"
+        (check-equal? (graphviz sg/an)
+                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode7 [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=\"'(z y x)\"];\n\t\tnode1 -> node6 [label=\"'(z y x)\"];\n\t\tnode2 -> node4 [label=\"'(z y x)\"];\n\t\tnode3 -> node6 [label=\"'(z y x)\"];\n\t\tnode4 -> node1 [label=\"'(z y x)\"];\n\t\tnode5 -> node7 [label=\"'(z y x)\"];\n\t\tnode6 -> node5 [label=\"'(z y x)\"];\n\t\tnode7 -> node1 [label=\"'(z y x)\"];\n\t}\n}\n"))
 
       (test-case "pretty-print-state-graph, pretty-print-state-graph/boolean"
         (check-equal? (graphviz (ppsg sg))
diff --git a/scribblings/networks.scrbl b/scribblings/networks.scrbl
index 55e5ae5..1927629 100644
--- a/scribblings/networks.scrbl
+++ b/scribblings/networks.scrbl
@@ -453,6 +453,8 @@ Creates the asynchronous dynamics for a given network: an instance of
 @racket[dynamics%] with @tt{network} as the network and the asynchronous
 mode as @tt{mode}.
 
+See @racket[build-full-state-graph/annotated] for an example.
+
 }
 
 @defproc[(make-syn-dynamics [network (Network a)]) (Dynamics% a)]{
@@ -480,6 +482,21 @@ Builds the full state graph of the given dynamics.
 
 }
 
+@defproc[(build-full-state-graph/annotated [dyn (Dynamics% a)]) Graph]{
+
+Builds the full annotated state graph of the given dynamics.
+
+@ex[
+(require (only-in "utils.rkt" dotit))
+
+(let* ([n (forms->boolean-network (hash 'a '(and a b)
+                                        'b '(not b)))]
+       [asyn-dynamics (make-asyn-dynamics n)])
+  (dotit ((inst build-full-state-graph/annotated Boolean) asyn-dynamics)))
+]
+
+}
+
 @section[#:tag "networks_Pretty_printing"]{Pretty printing}
 
 This section defines various functions for nicely formatting node and edge