From 160713b56b8a3e4b0f5b980c4268746410d4a12d Mon Sep 17 00:00:00 2001 From: Sergiu Ivanov Date: Fri, 28 Feb 2020 21:45:54 +0100 Subject: [PATCH] generic: Add dds-build-state-graph-annotated and dds-build-n-step-state-graph-annotated. --- generic.rkt | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/generic.rkt b/generic.rkt index 19635de..4fd82c4 100644 --- a/generic.rkt +++ b/generic.rkt @@ -15,7 +15,9 @@ [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-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 (contract-out [dds? (-> any/c boolean?)])) @@ -72,6 +74,9 @@ (for/set ([new-s (dds-step-one dds 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. (define-generics 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 ;; state graph with dds-step-one. (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? #:fallbacks @@ -119,3 +134,17 @@ dds states (in-range nsteps) dummy-annotated-dds-step-one)]) (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)))])