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

networks: Implement dds-step-one-annotated.

This commit is contained in:
Sergiu Ivanov 2020-02-23 14:11:55 +01:00
parent afb97eae7c
commit e7eb1fb09e
2 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
networks-tests.rkt
View File

@ -114,6 +114,9 @@
[s (st '((a . #t) (b . #f)))])
(check-equal? (dds-step-one asyn s) (set (st '((a . #f) (b . #f)))
(st '((a . #t) (b . #f)))))
(check-equal? (dds-step-one-annotated asyn s)
(set (cons (set 'b) '#hash((a . #t) (b . #f)))
(cons (set 'a) '#hash((a . #f) (b . #f)))))
(check-equal? (dds-step-one syn s) (set (st '((a . #f) (b . #f)))))
(check-equal? (dds-step asyn (set (st '((a . #t) (b . #t)))
(st '((a . #f) (b . #t)))))

8
networks.rkt
View File

@ -37,6 +37,7 @@
[make-asyn-dynamics (-> network? dynamics?)]
[make-syn-dynamics (-> network? dynamics?)]
[dds-step-one (-> dynamics? state? (set/c state?))]
[dds-step-one-annotated (-> dynamics? state? (set/c (cons/c modality? state?)))]
[dds-step (-> dynamics? (set/c state? #:kind 'dont-care) (set/c state?))])
;; Predicates
(contract-out [variable? (-> any/c boolean?)]
@ -268,7 +269,12 @@
#:methods gen:dds
[(define/match (dds-step-one dyn s)
[((dynamics network mode) s)
(for/set ([m mode]) (update network s m))])])
(for/set ([m mode]) (update network s m))])
;; Annotates each result state with the modality which lead to it.
(define/match (dds-step-one-annotated dyn s)
[((dynamics network mode) s)
(for/set ([m mode]) (cons m (update network s m)))])])
;;; Given a list of variables, builds the asynchronous mode (a set of
;;; singletons).