Generalize the type of build-state-graph* and build-state-graph*/annotated.

This commit is contained in:
Sergiu Ivanov 2022-09-10 18:55:03 +02:00
parent 45410176b7
commit ecc57a34fc
2 changed files with 8 additions and 5 deletions

View file

@ -29,9 +29,9 @@
(: build-state-graph/annotated (-> (Listof State) Graph))
(define/abstract/error (build-state-graph/annotated sts))
(: build-state-graph* (-> (Listof State) Integer Graph))
(: build-state-graph* (-> (Listof State) (U Integer 'full) Graph))
(define/abstract/error (build-state-graph* sts nsteps))
(: build-state-graph*/annotated (-> (Listof State) Integer Graph))
(: build-state-graph*/annotated (-> (Listof State) (U Integer 'full) Graph))
(define/abstract/error (build-state-graph*/annotated nsteps sts))
))

View file

@ -87,10 +87,12 @@ step/annotated].
}
@defmethod[(build-state-graph* [sts (Listof State)] [nsteps Integer]) Graph]{
@defmethod[(build-state-graph* [sts (Listof State)] [nsteps (U 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] steps.
produces the state graph reachable from the starting states @racket[nsteps]
steps. If @racket[nsteps] is @racket['full], constructs the full state
graph instead.
This method falls back to exploring the state graph with @method[dds% step].
@ -101,7 +103,8 @@ This method falls back to exploring the state graph with @method[dds% step].
Given a set of starting states and a number @racket[nsteps] of steps to run,
produces the labelled state graph reachable from the starting states
@racket[nsteps] steps.
@racket[nsteps] steps. If @racket[nsteps] is @racket['full], constructs the
full state graph instead.
This method falls back to exploring the state graph with @method[dds%
step/annotated].