generic: Add dds-build-state-graph and dds-build-n-step-state-graph.

Also provide a common fallback implementation.
This commit is contained in:
Sergiu Ivanov 2020-02-23 18:51:57 +01:00
parent ef76e143f2
commit 39575f39c2
3 changed files with 66 additions and 6 deletions

View File

@ -5,7 +5,7 @@
;;; Provides the definition of several generic interfaces for discrete
;;; dynamical systems.
(require racket/generic)
(require racket/generic graph)
(provide
;; Generics
@ -13,7 +13,9 @@
;; Functions
(contract-out [dds-step-one (-> dds? any/c (set/c any/c))]
[dds-step-one-annotated (-> dds? any/c (set/c (cons/c any/c any/c)))]
[dds-step (-> dds? (set/c any/c #:kind 'dont-care) (set/c any/c))])
[dds-step (-> dds? (set/c any/c #:kind 'dont-care) (set/c any/c))]
[dds-build-state-graph (-> dds? (set/c any/c #:kind 'dont-care) graph?)]
[dds-build-n-step-state-graph (-> dds? (set/c any/c #:kind 'dont-care) number? graph?)])
;; Predicates
(contract-out [dds? (-> any/c boolean?)]))
@ -22,6 +24,30 @@
(define (fallback-dds-step dds ss)
(apply set-union (for/list ([s ss]) (dds-step-one dds s))))
;;; Given a dds, a set of starting states, and a range whose length
;;; determines the number of steps to run, produces the state graph
;;; reachable from the starting steps in this many steps. This is a
;;; fallback for dds-build-state-graph and dds-build-n-step-state
;;; graph.
(define (fallback-dds-build-state-graph dds states step-range)
(for/fold ([edges empty]
[current-states states]
[visited-states states]
#:result (directed-graph edges))
([i step-range]
#:break (set-empty? current-states))
(for/fold ([new-edges empty]
[new-states (set)]
#:result (values
(append edges new-edges)
(set-subtract new-states visited-states)
(set-union current-states visited-states)))
([s current-states])
(let ([ss-next (dds-step-one dds s)])
(values
(append new-edges (for/list ([s-next ss-next]) (list s s-next)))
(set-union ss-next new-states))))))
;;; A discrete dynamical system.
(define-generics dds
;; Given a dds and a state, produce the next states of the dds.
@ -35,7 +61,23 @@
;; states reachable in one step. This method falls back to running
;; dds-step-one for all states.
(dds-step dds states)
;; Given a dds and a set of starting states, produces the state
;; graph reachable from the starting states. This method falls back
;; to exploring the state graph with dds-step-one.
(dds-build-state-graph dds states)
;; Given a dds, a set of starting states, and a number of steps to
;; run, produces the state graph reachable from the starting states
;; in this many steps. This method falls back to exploring the
;; state graph with dds-step-one.
(dds-build-n-step-state-graph dds states nsteps)
#:defined-predicate dds-implements?
#:fallbacks
[(define dds-step fallback-dds-step)])
[(define dds-step fallback-dds-step)
(define (dds-build-state-graph dds states)
;; Run fallback-dds-build-state-graph with an infinite range,
;; which will make it stop only when it has explored all the
;; state graph.
(fallback-dds-build-state-graph dds states (in-naturals)))
(define (dds-build-n-step-state-graph dds states nsteps)
(fallback-dds-build-state-graph dds states (in-range nsteps)))])

View File

@ -113,7 +113,9 @@
[syn (make-syn-dynamics n)]
[s (st '((a . #t) (b . #f)))]
[ss (set (st '((a . #t) (b . #t)))
(st '((a . #f) (b . #t))))])
(st '((a . #f) (b . #t))))]
[gr1 (dds-build-n-step-state-graph asyn (set s) 1)]
[gr-full (dds-build-state-graph asyn (set s))])
(check-equal? (dds-step-one asyn s) (set (st '((a . #f) (b . #f)))
(st '((a . #t) (b . #f)))))
(check-equal? (dds-step-one-annotated asyn s)
@ -122,4 +124,18 @@
(check-equal? (dds-step-one syn s) (set (st '((a . #f) (b . #f)))))
(check-equal? (dds-step asyn ss)
(set (st '((a . #f) (b . #t)))
(st '((a . #t) (b . #t)))))))
(st '((a . #t) (b . #t)))))
(check-true (has-vertex? gr1 #hash((a . #t) (b . #f))))
(check-true (has-vertex? gr1 #hash((a . #f) (b . #f))))
(check-false (has-vertex? gr1 #hash((a . #t) (b . #t))))
(check-true (has-edge? gr1 #hash((a . #t) (b . #f)) #hash((a . #f) (b . #f))))
(check-true (has-edge? gr1 #hash((a . #t) (b . #f)) #hash((a . #t) (b . #f))))
(check-false (has-edge? gr1 #hash((a . #f) (b . #f)) #hash((a . #t) (b . #f))))
(check-true (has-vertex? gr-full #hash((a . #t) (b . #f))))
(check-true (has-vertex? gr-full #hash((a . #f) (b . #f))))
(check-false (has-vertex? gr-full #hash((a . #t) (b . #t))))
(check-true (has-edge? gr-full #hash((a . #t) (b . #f)) #hash((a . #f) (b . #f))))
(check-true (has-edge? gr-full #hash((a . #t) (b . #f)) #hash((a . #t) (b . #f))))
(check-true (has-edge? gr-full #hash((a . #f) (b . #f)) #hash((a . #t) (b . #f))))
(check-true (has-edge? gr-full #hash((a . #f) (b . #f)) #hash((a . #f) (b . #f))))))

View File

@ -38,7 +38,9 @@
[make-syn-dynamics (-> network? dynamics?)]
[dds-step-one (-> dynamics? state? (set/c state?))]
[dds-step-one-annotated (-> dynamics? state? (set/c (cons/c modality? state?)))]
[dds-step (-> dynamics? (set/c state? #:kind 'dont-care) (set/c state?))])
[dds-step (-> dynamics? (set/c state? #:kind 'dont-care) (set/c state?))]
[dds-build-state-graph (-> dynamics? (set/c state? #:kind 'dont-care) graph?)]
[dds-build-n-step-state-graph (-> dynamics? (set/c state? #:kind 'dont-care) number? graph?)])
;; Predicates
(contract-out [variable? (-> any/c boolean?)]
[state? (-> any/c boolean?)]