2022-07-06 00:00:17 +02:00
|
|
|
#lang typed/racket
|
|
|
|
|
|
2022-08-23 10:17:58 +02:00
|
|
|
(require "utils.rkt" typed/graph)
|
|
|
|
|
|
|
|
|
|
(provide dds%)
|
|
|
|
|
|
|
|
|
|
(define dds%
|
|
|
|
|
(class object%
|
|
|
|
|
#:forall (State Modality)
|
|
|
|
|
(super-new)
|
|
|
|
|
|
|
|
|
|
(: step (-> State (Listof State)))
|
2022-09-02 16:32:52 +02:00
|
|
|
(define/public (step st)
|
|
|
|
|
(map (inst cdr Modality State) (step/annotated st)))
|
2022-08-23 10:17:58 +02:00
|
|
|
|
|
|
|
|
(: step/annotated (-> State (Listof (Pairof Modality State))))
|
|
|
|
|
(define/abstract/error (step/annotated st))
|
|
|
|
|
|
|
|
|
|
(: step* (-> (Listof State) (Listof State)))
|
|
|
|
|
(define/abstract/error (step* sts))
|
|
|
|
|
|
|
|
|
|
(: build-state-graph (-> (Listof State) Graph))
|
|
|
|
|
(define/abstract/error (build-state-graph sts))
|
|
|
|
|
|
|
|
|
|
(: build-state-graph/annotated (-> (Listof State) Graph))
|
|
|
|
|
(define/abstract/error (build-state-graph/annotated sts))
|
|
|
|
|
|
|
|
|
|
(: build-state-graph* (-> (Listof State) Integer Graph))
|
|
|
|
|
(define/abstract/error (build-state-graph* sts nsteps))
|
|
|
|
|
|
|
|
|
|
(: build-state-graph*/annotated (-> (Listof State) Integer Graph))
|
|
|
|
|
(define/abstract/error (build-state-graph*/annotated nsteps sts))
|
|
|
|
|
))
|
