dds/dynamics.rkt

69 lines
2.5 KiB
Racket
Raw Normal View History

2022-07-06 00:00:17 +02:00
#lang typed/racket
2022-08-23 10:17:58 +02:00
(require "utils.rkt" typed/graph)
(provide dds%)
(define dds%
(class object%
#:forall (State Modality)
(super-new)
(: step (-> State (Listof State)))
2022-09-02 16:32:52 +02:00
(define/public (step st)
(map (inst cdr Modality State) (step/annotated st)))
2022-08-23 10:17:58 +02:00
(: step/annotated (-> State (Listof (Pairof Modality State))))
(define/abstract/error (step/annotated st))
(: step* (-> (Listof State) (Listof State)))
2022-09-10 17:46:26 +02:00
(define/public (step* sts)
(remove-duplicates
(apply append
(for/list : (Listof (Listof State)) ([s sts])
(step s)))))
2022-08-23 10:17:58 +02:00
(: build-state-graph (-> (Listof State) Graph))
(define/public (build-state-graph sts)
(build-state-graph* sts 'full))
2022-08-23 10:17:58 +02:00
(: build-state-graph/annotated (-> (Listof State) Graph))
(define/public (build-state-graph/annotated sts)
(build-state-graph*/annotated sts 'full))
2022-08-23 10:17:58 +02:00
(: build-state-graph* (-> (Listof State) (U Positive-Integer 'full) Graph))
(define/public (build-state-graph* sts nsteps)
(unweighted-graph/directed
(assert-type (get-edges (build-state-graph*/annotated sts nsteps))
(Listof (List Any Any)))))
2022-08-23 10:17:58 +02:00
(: build-state-graph*/annotated (-> (Listof State) (U Positive-Integer 'full) Graph))
(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))))))
2022-08-23 10:17:58 +02:00
))