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") + ) ) ) )