generic: Add dds-step-one-annotated.

This commit is contained in:
Sergiu Ivanov 2020-02-23 14:11:38 +01:00
parent 5969595bed
commit afb97eae7c

View file

@ -12,6 +12,7 @@
gen:dds gen:dds
;; Functions ;; Functions
(contract-out [dds-step-one (-> dds? any/c (set/c any/c))] (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))])
;; Predicates ;; Predicates
(contract-out [dds? (-> any/c boolean?)])) (contract-out [dds? (-> any/c boolean?)]))
@ -25,6 +26,10 @@
(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.
(dds-step-one dds state) (dds-step-one dds state)
;; Given a dds and a state, produce the next states paired with some
;; annotation. Typical usage would include including the
;; information about the update mode.
(dds-step-one-annotated dds state)
;; Given a dds and a set of starting states, produce the set of ;; Given a dds and a set of starting states, produce the set of
;; states reachable in one step. This method falls back to running ;; states reachable in one step. This method falls back to running
;; dds-step-one for all states. ;; dds-step-one for all states.