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

This commit is contained in:
Sergiu Ivanov 2020-02-28 21:45:54 +01:00
parent 601e8ed8b3
commit 160713b56b

View file

@ -15,7 +15,9 @@
[dds-step-one-annotated (-> dds? any/c (set/c (cons/c any/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-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?)]) [dds-build-n-step-state-graph (-> dds? (set/c any/c #:kind 'dont-care) number? graph?)]
[dds-build-state-graph-annotated (-> dds? (set/c any/c #:kind 'dont-care) graph?)]
[dds-build-n-step-state-graph-annotated (-> dds? (set/c any/c #:kind 'dont-care) number? graph?)])
;; Predicates ;; Predicates
(contract-out [dds? (-> any/c boolean?)])) (contract-out [dds? (-> any/c boolean?)]))
@ -72,6 +74,9 @@
(for/set ([new-s (dds-step-one dds s)]) (for/set ([new-s (dds-step-one dds s)])
(cons 'dummy new-s))) (cons 'dummy new-s)))
;;; A poor man's fallback for dds-step-one-annotated.
(define (fallback-dds-step-one-annotated dds s) (dds-step-one-annotated dds s))
;;; A discrete dynamical system. ;;; A discrete dynamical system.
(define-generics dds (define-generics dds
;; Given a dds and a state, produce the next states of the dds. ;; Given a dds and a state, produce the next states of the dds.
@ -94,6 +99,16 @@
;; in this many steps. This method falls back to exploring the ;; in this many steps. This method falls back to exploring the
;; state graph with dds-step-one. ;; state graph with dds-step-one.
(dds-build-n-step-state-graph dds states nsteps) (dds-build-n-step-state-graph dds states nsteps)
;; Given a dds and a set of starting states, produces the labelled
;; state graph reachable from the starting states. This method
;; falls back to exploring the state graph with
;; dds-step-one-annotated.
(dds-build-state-graph-annotated dds states)
;; Given a dds, a set of starting states, and a number of steps to
;; run, produces the labelled state graph reachable from the
;; starting states in this many steps. This method falls back to
;; exploring the state graph with dds-step-one-annotated.
(dds-build-n-step-state-graph-annotated dds states nsteps)
#:defined-predicate dds-implements? #:defined-predicate dds-implements?
#:fallbacks #:fallbacks
@ -119,3 +134,17 @@
dds states (in-range nsteps) dds states (in-range nsteps)
dummy-annotated-dds-step-one)]) dummy-annotated-dds-step-one)])
(directed-graph edges))) (directed-graph edges)))
(define (dds-build-state-graph-annotated dds states)
(let-values ([(edges labels)
(fallback-dds-build-state-graph-edges
dds states (in-naturals)
fallback-dds-step-one-annotated)])
(directed-graph edges labels)))
(define (dds-build-n-step-state-graph-annotated dds states nsteps)
(let-values ([(edges labels)
(fallback-dds-build-state-graph-edges
dds states (in-range nsteps)
fallback-dds-step-one-annotated)])
(directed-graph edges labels)))])