scolobb/dds
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Refine the types of build-state-graph* and build-state-graph*/annotated.

Browse source
This commit is contained in:
Sergiu Ivanov 2022-09-15 01:11:11 +02:00
parent d7f4d2d732
commit 857b33ad71
2 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
dynamics.rkt
View file

@ -29,11 +29,10 @@
(: build-state-graph/annotated (-> (Listof State) Graph))
(define/abstract/error (build-state-graph/annotated sts))
(: build-state-graph* (-> (Listof State) (U Integer 'full) Graph))
(: build-state-graph* (-> (Listof State) (U Positive-Integer 'full) Graph))
(define/abstract/error (build-state-graph* sts nsteps))
(: build-state-graph*/annotated (-> (Listof State) (U Integer 'full) Graph))
;; TODO: Integer -> Positive-Integer
(: 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)

7
scribblings/dynamics.scrbl
View file

@ -87,7 +87,9 @@ step/annotated].
}
@defmethod[(build-state-graph* [sts (Listof State)] [nsteps (U Integer 'full)]) Graph]{
@defmethod[(build-state-graph* [sts (Listof State)]
[nsteps (U Positive-Integer 'full)])
Graph]{
Given a set of starting states and a number @racket[nsteps] of steps to run,
produces the state graph reachable from the starting states @racket[nsteps]
@ -98,7 +100,8 @@ This method falls back to exploring the state graph with @method[dds% step].
}
@defmethod[(build-state-graph*/annotated [sts (Listof State)] [nsteps Integer])
@defmethod[(build-state-graph*/annotated [sts (Listof State)]
[nsteps (U Positive-Integer 'full)])
Graph]{
Given a set of starting states and a number @racket[nsteps] of steps to run,