diff --git a/networks-tests.rkt b/networks-tests.rkt
index ce91a36..c5d4ce1 100644
--- a/networks-tests.rkt
+++ b/networks-tests.rkt
@@ -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)))))
diff --git a/networks.rkt b/networks.rkt
index 12a5ce0..df11fd3 100644
--- a/networks.rkt
+++ b/networks.rkt
@@ -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).