Implement build-state-graph*/annotated.

This commit is contained in:
Sergiu Ivanov 2022-09-15 00:57:38 +02:00
parent ecc57a34fc
commit d7f4d2d732
2 changed files with 34 additions and 1 deletions

View file

@ -33,5 +33,32 @@
(define/abstract/error (build-state-graph* sts nsteps)) (define/abstract/error (build-state-graph* sts nsteps))
(: build-state-graph*/annotated (-> (Listof State) (U Integer 'full) Graph)) (: 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))))))
)) ))

View file

@ -561,6 +561,12 @@
(check-equal? (list->set (send dyn-asyn step* (list s1 s2))) (check-equal? (list->set (send dyn-asyn step* (list s1 s2)))
(list->set (append (send dyn-asyn step s1) (list->set (append (send dyn-asyn step s1)
(send dyn-asyn step s2))))) (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")
)
) )
) )
) )