diff --git a/networks.rkt b/networks.rkt
index 3965374..06962fa 100644
--- a/networks.rkt
+++ b/networks.rkt
@@ -1,1342 +1,678 @@
-#lang racket
+#lang typed/racket
 
-(module typed typed/racket
-  (require "utils.rkt" "functions.rkt" "dynamics.rkt"
-           typed/graph typed/racket/random
-           syntax/parse/define)
-  (require/typed racket/syntax
-    [format-symbol (-> String Any * Symbol)])
-
-  (module+ test
-    (require typed/rackunit)
-    (define skip-expensive-tests? #t)
-    (unless skip-expensive-tests?
-      (displayln "Running the complete test suite...")))
-
-  (provide
-   State UpdateFunction Domain DomainMapping
-   01->boolean/state
-
-   (struct-out network) Network
-   make-same-domains make-boolean-domains make-boolean-network
-   make-01-domains make-01-network update
-
-   UpdateFunctionForm (struct-out network-form) NetworkForm
-   update-function-form->update-function/any
-   update-function-form->update-function/boolean
-   update-function-form->update-function/01
-   network-form->network/any network-form->network/boolean
-   network-form->network/01 make-boolean-network-form
-   forms->boolean-network
-
-   build-all-states build-all-boolean-states build-all-01-states
-
-   list-syntactic-interactions build-syntactic-interaction-graph
-   interaction? get-interaction-sign build-interaction-graph
-   build-interaction-graph/form build-signed-interaction-graph
-   build-signed-interaction-graph/form
-
-   Modality Mode dynamics% Dynamics% make-syn make-asyn
-   make-asyn-dynamics make-syn-dynamics build-full-state-graph
-   build-full-state-graph/annotated
-   pretty-print-state pretty-print-state/01 pretty-print-state-graph-with
-   pretty-print-state-graph ppsg pretty-print-state-graph/01 ppsg01
-
-   tabulate-state* tabulate-state*/boolean
-   tabulate-state*+headers tabulate-state*+headers/boolean
-   tabulate-state tabulate-state/boolean
-   tabulate-state+headers tabulate-state+headers/boolean
-   tabulate-network tabulate-network+headers
-
-   table+vars->network table->network table+headers->network
-
-   random-function/state random-boolean-function/state random-network
-   random-boolean-network random-boolean-network/n
-   )
-
-  (define-type (State a) (VariableMapping a))
-  (define-type (UpdateFunction a) (-> (State a) a))
-  (define-type (Domain a) (Listof a))
-  (define-type (DomainMapping a) (VariableMapping (Domain a)))
-
-  (: 01->boolean/state (-> (State (U Zero One)) (State Boolean)))
-  (define (01->boolean/state s)
-    (for/hash ([(x val) (in-hash s)]) : (State Boolean)
-              (if (eq? val 1) (values x #t) (values x #f))))
-
-  (module+ test
-    (test-case "01->boolean/state"
-      (check-equal? (01->boolean/state (hash 'a 0 'b 1))
-                    (hash 'a #f 'b #t))))
-
-  (struct (a) network ([functions : (VariableMapping (UpdateFunction a))]
-                       [domains : (DomainMapping a)])
-    #:transparent
-    #:type-name Network)
-
-  (: make-same-domains (All (a) (-> (Listof Variable) (Domain a)
-                                    (DomainMapping a))))
-  (define (make-same-domains vars domain)
-    (for/hash ([var vars]) : (DomainMapping a)
-              (values var domain)))
-
-  (module+ test
-    (test-case "make-same-domains"
-      (check-equal? (make-same-domains '(a b) '(1 2))
-                    #hash((a . (1 2)) (b . (1 2))))))
-
-  (: make-boolean-domains (-> (Listof Variable) (DomainMapping Boolean)))
-  (define (make-boolean-domains vars)
-    (make-same-domains vars '(#f #t)))
-
-  (module+ test
-    (test-case "make-boolean-domains"
-      (check-equal? (make-boolean-domains '(a b))
-                    #hash((a . (#f #t)) (b . (#f #t))))))
-
-  (: make-boolean-network (-> (VariableMapping (UpdateFunction Boolean))
-                              (Network Boolean)))
-  (define (make-boolean-network funcs)
-    (network funcs (make-boolean-domains (hash-keys funcs))))
-
-  (module+ test
-    (test-case "make-boolean-network"
-      (define f1 (λ ([s : (State Boolean)])
-                   (and (hash-ref s 'x1) (not (hash-ref s 'x2)))))
-      (define f2 (λ ([s : (State Boolean)])
-                   (not (hash-ref s 'x2))))
-      (define bn (make-boolean-network (hash 'x1 f1 'x2 f2)))
-      (check-equal? (network-domains bn) (hash 'x1 '(#f #t) 'x2 '(#f #t)))))
-
-  (: make-01-domains (-> (Listof Variable) (DomainMapping (U Zero One))))
-  (define (make-01-domains vars)
-    (make-same-domains vars '(0 1)))
-
-  (module+ test
-    (test-case "make-01-domains"
-      (check-equal? (make-01-domains '(a b))
-                    '#hash((a . (0 1)) (b . (0 1))))))
-
-  (: make-01-network (-> (VariableMapping (UpdateFunction (U Zero One)))
-                         (Network (U Zero One))))
-  (define (make-01-network funcs)
-    (network funcs (make-01-domains (hash-keys funcs))))
-
-  (module+ test
-    (test-case "make-01-network"
-      (define f1 (λ ([s : (State (U Zero One))])
-                   (assert-type (max (hash-ref s 'a) (hash-ref s 'b))
-                                (U Zero One))))
-      (define f2 (λ ([s : (State (U Zero One))])
-                   (assert-type (min (hash-ref s 'a) (hash-ref s 'b))
-                                (U Zero One))))
-      (define n (make-01-network (hash 'a f1 'b f2)))
-      (check-equal? (network-domains n) (hash 'a '(0 1) 'b '(0 1)))))
-
-  (: update (All (a) (-> (Network a) (State a) (Listof Variable) (State a))))
-  (define (update network s xs)
-    (define funcs (network-functions network))
-    (for/fold ([new-s : (State a) s])
-              ([x xs])
-      (define fx (hash-ref funcs x))
-      (hash-set new-s x (fx s))))
-
-  (module+ test
-    (test-case "update"
-      (define f1 (λ ([s : (State Boolean)])
-                   (and (hash-ref s 'x1) (not (hash-ref s 'x2)))))
-      (define f2 (λ ([s : (State Boolean)])
-                   (not (hash-ref s 'x2))))
-      (define bn (make-boolean-network (hash 'x1 f1 'x2 f2)))
-      (check-equal? (update bn (hash 'x1 #f 'x2 #f) '(x1))
-                    #hash((x1 . #f) (x2 . #f)))
-      (check-equal? (update bn (hash 'x1 #f 'x2 #f) '(x1 x2))
-                    #hash((x1 . #f) (x2 . #t)))))
-
-  (define-type UpdateFunctionForm Any)
-
-  (struct (a) network-form ([forms : (VariableMapping UpdateFunctionForm)]
-                            [domains : (DomainMapping a)])
-    #:transparent
-    #:type-name NetworkForm)
-
-  (: update-function-form->update-function/any (-> UpdateFunctionForm (UpdateFunction Any)))
-  (define (update-function-form->update-function/any form)
-    (λ (s) (eval1-with s form)))
-
-  (module+ test
-    (test-case "update-function-form->update-function/any"
-      (define s (hash 'x #t 'y #f))
-      (define f (update-function-form->update-function/any '(and x y)))
-      (check-equal? (f s) #f)))
-
-  (: update-function-form->update-function/boolean (-> UpdateFunctionForm (UpdateFunction Boolean)))
-  (define (update-function-form->update-function/boolean form)
-    (λ (s) (assert-type (eval1-with s form) Boolean)))
-
-  (module+ test
-    (test-case "update-function-form->update-function/boolean"
-      (define s (hash 'x #t 'y #f))
-      (define f (update-function-form->update-function/boolean '(and x y)))
-      (check-equal? (f s) #f)))
-
-  (: update-function-form->update-function/01 (-> UpdateFunctionForm (UpdateFunction (U Zero One))))
-  (define (update-function-form->update-function/01 form)
-    (λ (s) (assert-type (eval1-with s form) (U Zero One))))
-
-  (module+ test
-    (test-case "update-function-form->update-function/01"
-      (define s (hash 'x 0 'y 1))
-      (define f (update-function-form->update-function/01 '(max x y)))
-      (check-equal? (f s) 1)))
-
-  (: network-form->network/any (-> (NetworkForm Any) (Network Any)))
-  (define (network-form->network/any nf)
-    (network
-     (for/hash ([(x form) (in-hash (network-form-forms nf))])
-       : (VariableMapping (UpdateFunction Any))
-       (values x (update-function-form->update-function/any form)))
-     (network-form-domains nf)))
-
-  (module+ test
-    (test-case "network-form->network/any"
-      (define bn (network-form->network/any
-                  (network-form (hash 'a '(and a b)
-                                      'b '(not b))
-                                (hash 'a '(#f #t)
-                                      'b '(#f #t)))))
-      (define s (hash 'a #t 'b #t))
-      (check-equal? ((hash-ref (network-functions bn) 'a) s) #t)))
-
-  (: network-form->network/boolean (-> (NetworkForm Boolean) (Network Boolean)))
-  (define (network-form->network/boolean nf)
-    (network
-     (for/hash ([(x form) (in-hash (network-form-forms nf))])
-       : (VariableMapping (UpdateFunction Boolean))
-       (values x (update-function-form->update-function/boolean form)))
-     (network-form-domains nf)))
-
-  (module+ test
-    (test-case "network-form->network/boolean"
-      (define bn (network-form->network/boolean
-                  (network-form (hash 'a '(and a b)
-                                      'b '(not b))
-                                (hash 'a '(#f #t)
-                                      'b '(#f #t)))))
-      (define s (hash 'a #t 'b #t))
-      (check-equal? ((hash-ref (network-functions bn) 'a) s) #t)))
-
-  (: network-form->network/01 (-> (NetworkForm (U Zero One)) (Network (U Zero One))))
-  (define (network-form->network/01 nf)
-    (network
-     (for/hash ([(x form) (in-hash (network-form-forms nf))])
-       : (VariableMapping (UpdateFunction (U Zero One)))
-       (values x (update-function-form->update-function/01 form)))
-     (network-form-domains nf)))
-
-  (module+ test
-    (test-case "network-form->network/01"
-      (define bn (network-form->network/01
-                  (network-form (hash 'a '(min a b)
-                                      'b '(- 1 b))
-                                (hash 'a '(0 1)
-                                      'b '(0 1)))))
-      (define s (hash 'a 1 'b 1))
-      (check-equal? ((hash-ref (network-functions bn) 'a) s) 1)))
-
-  (: make-boolean-network-form (-> (VariableMapping UpdateFunctionForm)
-                                   (NetworkForm Boolean)))
-  (define (make-boolean-network-form forms)
-    (network-form forms (make-boolean-domains (hash-keys forms))))
-
-  (module+ test
-    (test-case "make-boolean-network-form"
-      (check-equal? (make-boolean-network-form (hash 'a '(and a b)
-                                                     'b '(not b)))
-                    (network-form
-                     '#hash((a . (and a b)) (b . (not b)))
-                     '#hash((a . (#f #t)) (b . (#f #t)))))))
-
-  (: forms->boolean-network (-> (VariableMapping UpdateFunctionForm)
-                                (Network Boolean)))
-  (define forms->boolean-network
-    (compose network-form->network/boolean make-boolean-network-form))
-
-  (module+ test
-    (test-case "forms->boolean-network"
-      (define n (forms->boolean-network (hash 'a '(and a b)
-                                              'b '(not b))))
-      (check-equal? (network-domains n) (hash 'a '(#f #t)
-                                              'b '(#f #t)))))
-
-  (: build-all-states (All (a) (-> (DomainMapping a) (Listof (State a)))))
-  (define (build-all-states vars-domains)
-    ;; TODO: Use hash-keys and hash-values when Typed Racket will have
-    ;; caught up with the new argument try-order?.
-    (define vdlist (hash-map vars-domains (inst cons Variable (Domain a)) #t))
-    (define vars (map (inst car Variable (Domain a)) vdlist))
-    (define doms (map (inst cdr Variable (Domain a)) vdlist))
-    (for/list ([s (apply cartesian-product doms)])
-      (make-immutable-hash (map (inst cons Variable a) vars s))))
-
-  (module+ test
-    (test-case "build-all-states"
-      (check-equal? (build-all-states #hash((a . (#t #f)) (b . (1 2 3))))
-                    '(#hash((a . #t) (b . 1))
-                      #hash((a . #t) (b . 2))
-                      #hash((a . #t) (b . 3))
-                      #hash((a . #f) (b . 1))
-                      #hash((a . #f) (b . 2))
-                      #hash((a . #f) (b . 3))))))
-
-  (: build-all-boolean-states (-> (Listof Variable) (Listof (State Boolean))))
-  (define (build-all-boolean-states vars)
-    (build-all-states (make-boolean-domains vars)))
-
-  (module+ test
-    (test-case "build-all-boolean-states"
-      (check-equal? (build-all-boolean-states '(a b))
-                    '(#hash((a . #f) (b . #f))
-                      #hash((a . #f) (b . #t))
-                      #hash((a . #t) (b . #f))
-                      #hash((a . #t) (b . #t))))))
-
-  (: build-all-01-states (-> (Listof Variable) (Listof (State (U Zero One)))))
-  (define (build-all-01-states vars)
-    (build-all-states (make-01-domains vars)))
-
-  (module+ test
-    (test-case "build-all-01-states"
-      (check-equal? (build-all-01-states '(a b))
-                    '(#hash((a . 0) (b . 0))
-                      #hash((a . 0) (b . 1))
-                      #hash((a . 1) (b . 0))
-                      #hash((a . 1) (b . 1))))))
-
-  (: list-syntactic-interactions
-     (All (a) (-> (NetworkForm a) Variable (Listof Variable))))
-  (define (list-syntactic-interactions nf x)
-    (set-intersect
-     (extract-symbols (hash-ref (network-form-forms nf) x))
-     (hash-keys (network-form-forms nf))))
-
-  (module+ test
-    (test-case "list-syntactic-interactions"
-      (define n (make-boolean-network-form #hash((a . (+ a b c))
-                                                 (b . (- b c)))))
-      (check-true (set=? (list-syntactic-interactions n 'a) '(a b)))
-      (check-true (set=? (list-syntactic-interactions n 'b) '(b)))))
-
-  (: build-syntactic-interaction-graph (All (a) (-> (NetworkForm a) Graph)))
-  (define (build-syntactic-interaction-graph n)
-    (transpose
-     (unweighted-graph/adj
-      (for/list ([(var _) (in-hash (network-form-forms n))])
-        (cons var (list-syntactic-interactions n var))))))
-
-  (module+ test
-    (test-case "build-syntactic-interaction-graph"
-      (define n (make-boolean-network-form #hash((a . (+ a b c))
-                                                 (b . (- b c)))))
-      (define ig (build-syntactic-interaction-graph n))
-      (check-true (has-vertex? ig 'a))
-      (check-true (has-vertex? ig 'b))
-      (check-false (has-vertex? ig 'c))
-      (check-true (has-edge? ig 'a 'a))
-      (check-true (has-edge? ig 'b 'a))
-      (check-true (has-edge? ig 'b 'b))
-      (check-false (has-edge? ig 'c 'b))
-      (check-false (has-edge? ig 'c 'a))))
-
-  (: interaction? (All (a) (-> (Network a) Variable Variable Boolean)))
-  (define (interaction? network x y)
-    (define doms (network-domains network))
-    (define states-not-x (build-all-states (hash-remove doms x)))
-    (define dom-x (hash-ref doms x))
-    (define y-func (hash-ref (network-functions network) y))
-    (: different-ys-exist? (-> (State a) Boolean))
-    (define (different-ys-exist? st)
-      (define x-states (for/list ([x-val (in-list dom-x)])
-                         : (Listof (State a))
-                         (hash-set st x x-val)))
-      ;; TODO: Replace with for*/first when/if it is fixed.
-      (for*/first/typed : (Option Boolean)
-                        ([st1 : (State a) x-states]
-                         [st2 : (State a) x-states]
-                         #:unless (equal? (hash-ref st1 x) (hash-ref st2 x))
-                         #:unless (equal? (y-func st1) (y-func st2)))
-        #t))
-    ;; TODO: Replace with for/first when/if it is fixed.
-    (for/first/typed : (Option Boolean)
-                     ([st (in-list states-not-x)]
-                      #:when (different-ys-exist? st))
-      #t))
-
-  (module+ test
-    (test-case "interaction?"
-      (define n1 (forms->boolean-network
-                  (hash 'x '(not y)
-                        'y 'x
-                        'z '(and y z))))
-      (check-true (interaction? n1 'x 'y))
-      (check-true (interaction? n1 'y 'x))
-      (check-false (interaction? n1 'x 'z))
-      (define n-multi (hash 'x '(max (+ y 1) 2)
-                            'y '(min (- y 1) 0)))
-      (define 123-doms (make-same-domains '(x y) '(0 1 2)))
-      (define n2 (network-form->network/any (network-form n-multi 123-doms)))
-      (check-false (interaction? n2 'x 'y))
-      (check-true (interaction? n2 'y 'x))))
-
-  (: get-interaction-sign (All (a) (-> (Network a) Variable Variable (Option Integer))))
-  (define (get-interaction-sign network x y)
-    (define doms (network-domains network))
-    (define dom-x (hash-ref doms x))
-    (define dom-y (hash-ref doms y))
-    (define y-func (hash-ref (network-functions network) y))
-    (define (collect-impacts-on-y [st : (State a)])
-      ;; The way in which the values are ordered in the domains gives
-      ;; a total order on these values.  This means that considering
-      ;; pairs of consecutive values of x is sufficient for testing the
-      ;; sign of the interaction.
-      (define x-states (for/list : (Listof (State a))
-                                 ([x-val (in-list dom-x)])
-                         (hash-set st x x-val)))
-      (for/list : (Listof (U '< '> '=))
-                ([st1 (in-list x-states)]
-                 [st2 (in-list (cdr x-states))])
-        (define y1-idx (assert-type (index-of dom-y (y-func st1)) Index))
-        (define y2-idx (assert-type (index-of dom-y (y-func st2)) Index))
-        (cond
-          [(< y1-idx y2-idx) '<]
-          [(> y1-idx y2-idx) '>]
-          [else '=])))
-    (define states-not-x (build-all-states (hash-remove doms x)))
-    (define interactions
-      (remove-duplicates
-       (for/list : (Listof (U '< '> '= Zero))
-                 ([st (in-list states-not-x)])
-         (define impacts (remove-duplicates (collect-impacts-on-y st)))
-         (cond
-           [(and (member '< impacts) (not (member '> impacts))) '<]
-           [(and (member '> impacts) (not (member '< impacts))) '>]
-           [(equal? impacts '(=)) '=]
-           [else 0]))))
-    (cond
-      [(and (member '< interactions) (not (member '> interactions))) 1]
-      [(and (member '> interactions) (not (member '< interactions))) -1]
-      [(equal? interactions '(=)) #f]
-      [else 0]))
-
-  (module+ test
-    (test-case "get-interaction-sign"
-      (define n1 (forms->boolean-network
-                  (hash 'x '(not y)
-                        'y 'x
-                        'z '(and y z)
-                        't '(or (and (not x) y)
-                                (and x (not y))))))
-      (check-equal? (get-interaction-sign n1 'x 'y) 1)
-      (check-equal? (get-interaction-sign n1 'y 'x) -1)
-      (check-false (get-interaction-sign n1 'x 'z))
-      (check-equal? (get-interaction-sign n1 'y 'z) 1)
-      (check-equal? (get-interaction-sign n1 'x 't) 0)
-      (define n-multi (hash 'x '(min (+ y 1) 2)
-                            'y '(max (- y 1) 0)
-                            'z '(- 2 y)
-                            't '(abs (- y 1))))
-      (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
-      (define n2 (network-form->network/any (network-form n-multi 123-doms)))
-      (check-false (get-interaction-sign n2 'x 'y))
-      (check-equal? (get-interaction-sign n2 'y 'x) 1)
-      (check-equal? (get-interaction-sign n2 'y 'z) -1)
-      (check-equal? (get-interaction-sign n2 'y 't) 0)
-      (check-equal? (get-interaction-sign n2 'y 'y) 1)))
-
-  (: build-interaction-graph (All (a) (-> (Network a) Graph)))
-  (define (build-interaction-graph network)
-    (define vars (hash-keys (network-functions network)))
-    (unweighted-graph/directed
-     (for*/list : (Listof (List Any Any))
-                ([x (in-list vars)]
-                 [y (in-list vars)]
-                 #:when (interaction? network x y))
-       (list x y))))
-
-  (: build-interaction-graph/form (All (a) (-> (NetworkForm a) Graph)))
-  (define (build-interaction-graph/form form)
-    (build-interaction-graph (network-form->network/any form)))
-
-  (module+ test
-    (test-case "build-interaction-graph"
-      (cond
-        [skip-expensive-tests?
-         (displayln "Skipping test case build-interaction-graph.")]
-        [else
-         (define n1 (make-boolean-network-form
-                     (hash 'x '(not y)
-                           'y 'x
-                           'z '(and y z)
-                           't '(or (and (not x) y)
-                                   (and x (not y))))))
-         (check-equal? (graphviz (build-interaction-graph/form n1))
-                       "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node3 [];\n\t\tnode2 -> node2 [];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [];\n\t\tnode0 -> node2 [];\n\t\tnode3 -> node1 [];\n\t}\n}\n")
-         (define n-multi (hash 'x '(min (+ y 1) 2)
-                               'y '(max (- y 1) 0)
-                               'z '(- 2 y)
-                               't '(abs (- y 1))))
-         (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
-         (define n2 (network-form n-multi 123-doms))
-         (check-equal? (graphviz (build-interaction-graph/form n2))
-                       "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [];\n\t\tnode0 -> node2 [];\n\t\tnode0 -> node3 [];\n\t}\n}\n")])))
-
-  (: build-signed-interaction-graph (All (a) (-> (Network a) Graph)))
-  (define (build-signed-interaction-graph network)
-    (define vars (hash-keys (network-functions network)))
-    (weighted-graph/directed
-     (for*/list : (Listof (List Integer Any Any))
-         ([x (in-list vars)]
-          [y (in-list vars)]
-          [sign (in-value (get-interaction-sign network x y))]
-          #:unless (eq? sign #f))
-       (list sign x y))))
-
-  (: build-signed-interaction-graph/form (All (a) (-> (NetworkForm a) Graph)))
-  (define (build-signed-interaction-graph/form nf)
-    (build-signed-interaction-graph (network-form->network/any nf)))
-
-  (module+ test
-    (test-case "build-signed-interaction-graph"
-      (cond
-        [skip-expensive-tests?
-         (displayln "Skipping test case build-signed-interaction-graph.")]
-        [else
-         (define n1 (make-boolean-network-form
-                     (hash 'x '(not y)
-                           'y 'x
-                           'z '(and y z)
-                           't '(or (and (not x) y)
-                                   (and x (not y))))))
-         (check-equal? (graphviz (build-signed-interaction-graph/form n1))
-                       "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode2 -> node2 [label=\"1\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"0\"];\n\t\tnode0 -> node2 [label=\"1\"];\n\t\tnode0 -> node3 [label=\"-1\"];\n\t\tnode3 -> node1 [label=\"0\"];\n\t\tnode3 -> node0 [label=\"1\"];\n\t}\n}\n")
-         (define n-multi (hash 'x '(min (+ y 1) 2)
-                               'y '(max (- y 1) 0)
-                               'z '(- 2 y)
-                               't '(abs (- y 1))))
-         (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
-         (define n2 (network-form n-multi 123-doms))
-         (check-equal? (graphviz (build-signed-interaction-graph/form n2))
-                       "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [label=\"1\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"0\"];\n\t\tnode0 -> node2 [label=\"-1\"];\n\t\tnode0 -> node3 [label=\"1\"];\n\t}\n}\n")])))
-
-  (define-type Modality (Listof Variable))
-  (define-type Mode (Listof Modality))
-
-  (define dynamics%
-    ;; TODO: Fix the parameter of State when Typed Racket supports
-    ;; passing type parameters to the parent.
-    (class (inst dds% (State Any) Modality)
-      #:forall (a)
-      (super-new)
-
-      (init-field [network : (Network a) network]
-                  [mode : Mode mode])
-
-      (: step/annotated (-> (State a) (Listof (Pairof Modality (State a)))))
-      (define/override (step/annotated s)
-        (for/list ([m mode])
-          (cons m (update network s m))))))
-
-  ;; TODO: Find a better way to define the type of the class
-  ;; dynamics%.
-  ;;
-  ;; TODO: Fix the parameter of State when Typed Racket supports
-  ;; passing type parameters to the parent.
-  ;;
-  ;; NOTE: The type appearing when you type dynamics% in the REPL does
-  ;; not directly type check, probably because of the structure types
-  ;; which are fully expanded in the REPL.
-  (define-type (Dynamics% a)
-    (Instance (Class
-               (init (network (Network a) #:optional)
-                     (mode Mode #:optional))
-               (field (network (Network a))
-                      (mode Mode))
-               (step (-> (State Any) (Listof (State Any))))
-               (step/annotated (-> (State a) (Listof (Pairof Modality (State a)))))
-               (step* (-> (Listof (State Any)) (Listof (State Any))))
-               (build-state-graph (-> (Listof (State Any)) Graph))
-               (build-state-graph/annotated (-> (Listof (State Any)) Graph))
-               (build-state-graph* (-> (Listof (State Any)) (U Positive-Integer 'full) Graph))
-               (build-state-graph*/annotated (-> (Listof (State Any)) (U Positive-Integer 'full) Graph)))))
-
-  (module+ test
-    (let* ([n1 : (Network Boolean)
-               (forms->boolean-network (hash 'x '(not y)
-                                             'y 'x
-                                             'z '(and y z)))]
-           [syn : Mode '((x y z))]
-           [asyn : Mode '((x) (y) (z))]
-           [dyn-syn (new (inst dynamics% Boolean) [network n1] [mode syn])]
-           [dyn-asyn (new (inst dynamics% Boolean) [network n1] [mode asyn])]
-           [s1 (hash 'x #f 'y #f 'z #f)]
-           [s2 (hash 'x #t 'y #t 'z #t)])
-      (test-case "dynamics%"
-        (check-equal? (send dyn-syn step/annotated s1)
-                      '(((x y z) . #hash((x . #t) (y . #f) (z . #f)))))
-        (check-equal? (send dyn-asyn step/annotated s1)
-                      '(((x) . #hash((x . #t) (y . #f) (z . #f)))
-                        ((y) . #hash((x . #f) (y . #f) (z . #f)))
-                        ((z) . #hash((x . #f) (y . #f) (z . #f))))))
-
-      (test-case "dynamics%:step"
-        (check-equal? (send dyn-syn step s1)
-                      '(#hash((x . #t) (y . #f) (z . #f))))
-        (check-equal? (send dyn-asyn step s1)
-                      '(#hash((x . #t) (y . #f) (z . #f))
-                        #hash((x . #f) (y . #f) (z . #f))
-                        #hash((x . #f) (y . #f) (z . #f)))))
-      (test-case "dynamics%:step*"
-        (check-equal? (list->set (send dyn-syn step* (list s1 s2)))
-                      (list->set (append (send dyn-syn step s1)
-                                         (send dyn-syn step s2))))
-        (check-equal? (list->set (send dyn-asyn step* (list s1 s2)))
-                      (list->set (append (send dyn-asyn step s1)
-                                         (send dyn-asyn step s2)))))
-      (test-case "dynamics%:build-state-graph*/annotated"
-        (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 2))
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"'(x y z)\"];\n\t\tnode2 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
-        (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 'full))
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [label=\"'(x y z)\"];\n\t\tnode1 -> node3 [label=\"'(x y z)\"];\n\t\tnode2 -> node1 [label=\"'(x y z)\"];\n\t\tnode3 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
-        )
-      (test-case "dynamics%:build-state-graph*"
-        (check-equal? (graphviz (send dyn-syn build-state-graph* (list s1) 2))
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [];\n\t\tnode1 -> node0 [];\n\t}\n}\n")
-        (check-equal? (graphviz (send dyn-syn build-state-graph* (list s1) 'full))
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node3 [];\n\t\tnode1 -> node0 [];\n\t\tnode2 -> node1 [];\n\t\tnode3 -> node2 [];\n\t}\n}\n"))
-      (test-case "dynamics%:build-state-graph/annotated"
-        (check-equal? (graphviz (send dyn-syn build-state-graph/annotated (list s1)))
-                      (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 'full))))
-      (test-case "dynamics%:build-state-graph"
-        (check-equal? (graphviz (send dyn-syn build-state-graph (list s1)))
-                      (graphviz (send dyn-syn build-state-graph* (list s1) 'full))))))
-
-  (: make-asyn (-> (Listof Variable) Mode))
-  (define (make-asyn vars) (map (inst list Variable) vars))
-
-  (module+ test
-    (test-case "make-asyn"
-      (check-equal? (make-asyn '(x y z)) '((x) (y) (z)))))
-
-  (: make-syn (-> (Listof Variable) Mode))
-  (define (make-syn vars) (list vars))
-
-  (module+ test
-    (test-case "make-syn"
-      (check-equal? (make-syn '(x y z)) '((x y z)))))
-
-  ;;; Given a network, applies a function for building a mode to its
-  ;;; variables and returns the corresponding network dynamics.
-  (: make-dynamics-from-mode
-     (All (a) (-> (Network a) (-> (Listof Variable) Mode) (Dynamics% a))))
-  (define (make-dynamics-from-mode n make-mode)
-    (new (inst dynamics% a)
-         [network n]
-         [mode (make-mode (hash-keys (network-functions n)))]))
-
-  (: make-asyn-dynamics (All (a) (-> (Network a) (Dynamics% a))))
-  (define (make-asyn-dynamics [n : (Network a)])
-    ((inst make-dynamics-from-mode a) n make-asyn))
-
-  (module+ test
-    (test-case "make-asyn-dynamics"
-      (define n : (Network Boolean)
-        (forms->boolean-network (hash 'x '(not y)
-                                      'y 'x
-                                      'z '(and y z))))
-      (define asyn-dyn (make-asyn-dynamics n))
-      (check-equal? (get-field network asyn-dyn) n)
-      (check-true (set=? (get-field mode asyn-dyn) '((x) (y) (z))))))
-
-  (: make-syn-dynamics (All (a) (-> (Network a) (Dynamics% a))))
-  (define (make-syn-dynamics [n : (Network a)])
-    ((inst make-dynamics-from-mode a) n make-syn))
-
-  (module+ test
-    (test-case "make-syn-dynamics"
-      (define n : (Network Boolean)
-        (forms->boolean-network (hash 'x '(not y)
-                                      'y 'x
-                                      'z '(and y z))))
-      (define syn-dyn (make-syn-dynamics n))
-      (check-equal? (get-field network syn-dyn) n)
-      (define m (get-field mode syn-dyn))
-      (check-equal? (length m) 1)
-      (check-true (set=? (car m) '(x y z)))))
-
-  (: pretty-print-state (All (a) (-> (State a) String)))
-  (define (pretty-print-state s)
-    (string-join (hash-map s (λ (key val) (format "~a:~a" key val)) #t)))
-
-  (module+ test
-    (test-case "pretty-print-state"
-      (check-equal? (pretty-print-state (hash 'a #f 'b 3 'c 4))
-                    "a:#f b:3 c:4")))
-
-  (: pretty-print-state/01 (All (a) (-> (State a) String)))
-  (define (pretty-print-state/01 s)
-    (string-join (hash-map s (λ (key val) (format "~a:~a" key (any->01 val))) #t)))
-
-  (module+ test
-    (test-case "pretty-print-state/01"
-      (check-equal?
-       (pretty-print-state/01 (hash 'a #f 'b #t 'c #t))
-       "a:0 b:1 c:1")))
-
-  (: pretty-print-state-graph-with (-> Graph (-> Any Any) Graph))
-  (define (pretty-print-state-graph-with gr pprinter)
-    (update-graph
-     gr
-     #:v-func pprinter
-     #:e-func (relax-arg-type/any pretty-print-set-sets (Setof (Setof Any)))))
-
-  (: pretty-print-state-graph (-> Graph Graph))
-  (define (pretty-print-state-graph gr)
-    (define (pprinter/any [x : Any])
-      (pretty-print-state (assert-type x (State Any))))
-    (pretty-print-state-graph-with
-     gr
-     (relax-arg-type/any pretty-print-state (State Any))))
-
-  (define ppsg pretty-print-state-graph)
-
-  (: pretty-print-state-graph/01 (-> Graph Graph))
-  (define (pretty-print-state-graph/01 gr)
-    (define (pprinter/any [x : Any])
-      (pretty-print-state/01 (assert-type x (State Any))))
-    (pretty-print-state-graph-with gr pprinter/any))
-
-  (define ppsg01 pretty-print-state-graph/01)
-
-  (: build-full-state-graph (All (a) (-> (Dynamics% a) Graph)))
-  (define (build-full-state-graph dyn)
-    (send dyn
-          build-state-graph
-          (build-all-states (network-domains (get-field network dyn)))))
-
-  (: build-full-state-graph/annotated (All (a) (-> (Dynamics% a) Graph)))
-  (define (build-full-state-graph/annotated dyn)
-    (send dyn
-          build-state-graph/annotated
-          (build-all-states (network-domains (get-field network dyn)))))
-
-  (module+ test
-    (let* ([n1 : (Network Boolean)
-               (forms->boolean-network (hash 'x '(not y)
-                                             'y 'x
-                                             'z '(and y z)))]
-           [dyn-syn (make-syn-dynamics n1)]
-           [sg ((inst build-full-state-graph Boolean) dyn-syn)]
-           [sg/an ((inst build-full-state-graph/annotated Boolean) dyn-syn)])
-      (test-case "build-full-state-graph"
-        (check-equal? (graphviz sg)
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode7 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [];\n\t\tnode1 -> node7 [];\n\t\tnode2 -> node4 [];\n\t\tnode3 -> node7 [];\n\t\tnode4 -> node1 [];\n\t\tnode5 -> node1 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node6 [];\n\t}\n}\n"))
-      (test-case "build-full-state-graph/annotated"
-        (check-equal? (graphviz sg/an)
-                      "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode7 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [label=\"'(z y x)\"];\n\t\tnode1 -> node6 [label=\"'(z y x)\"];\n\t\tnode2 -> node4 [label=\"'(z y x)\"];\n\t\tnode3 -> node6 [label=\"'(z y x)\"];\n\t\tnode4 -> node1 [label=\"'(z y x)\"];\n\t\tnode5 -> node7 [label=\"'(z y x)\"];\n\t\tnode6 -> node5 [label=\"'(z y x)\"];\n\t\tnode7 -> node1 [label=\"'(z y x)\"];\n\t}\n}\n"))
-
-      (test-case "pretty-print-state-graph, pretty-print-state-graph/boolean"
-        (check-equal? (graphviz (ppsg sg))
-                      "digraph G {\n\tnode0 [label=\"x:#f y:#t z:#f\"];\n\tnode1 [label=\"x:#f y:#t z:#t\"];\n\tnode2 [label=\"x:#t y:#f z:#t\"];\n\tnode3 [label=\"x:#t y:#t z:#t\"];\n\tnode4 [label=\"x:#t y:#t z:#f\"];\n\tnode5 [label=\"x:#t y:#f z:#f\"];\n\tnode6 [label=\"x:#f y:#f z:#f\"];\n\tnode7 [label=\"x:#f y:#f z:#t\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node6 [];\n\t\tnode1 -> node7 [];\n\t\tnode2 -> node4 [];\n\t\tnode3 -> node1 [];\n\t\tnode4 -> node0 [];\n\t\tnode5 -> node4 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node5 [];\n\t}\n}\n")
-        (check-equal? (graphviz (ppsg01 sg))
-                      "digraph G {\n\tnode0 [label=\"x:1 y:0 z:0\"];\n\tnode1 [label=\"x:0 y:1 z:1\"];\n\tnode2 [label=\"x:0 y:0 z:1\"];\n\tnode3 [label=\"x:1 y:1 z:1\"];\n\tnode4 [label=\"x:1 y:0 z:1\"];\n\tnode5 [label=\"x:0 y:1 z:0\"];\n\tnode6 [label=\"x:0 y:0 z:0\"];\n\tnode7 [label=\"x:1 y:1 z:0\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node7 [];\n\t\tnode1 -> node2 [];\n\t\tnode2 -> node0 [];\n\t\tnode3 -> node1 [];\n\t\tnode4 -> node7 [];\n\t\tnode5 -> node6 [];\n\t\tnode6 -> node0 [];\n\t\tnode7 -> node5 [];\n\t}\n}\n"))))
-
-  (: tabulate-state* (All (a) (-> (Listof (-> (State a) a)) (DomainMapping a)
-                                  (Listof (Listof a)))))
-  (define (tabulate-state* funcs domains)
-    (for/list : (Listof (Listof a)) ([s (in-list (build-all-states domains))])
-      (append (hash-map s (λ ([x : Variable] [y : a]) y) #t)
-              (for/list : (Listof a) ([f (in-list funcs)]) (f s)))))
-
-  (module+ test
-    (test-case "tabulate-state*"
-      (define/: f1 (State Integer) (+ :a :b))
-      (define/: f2 (State Integer) (- :a :b))
-      (check-equal? (tabulate-state* (list f1 f2) (hash 'a '(1 2) 'b '(2 3)))
-                    '((1 2 3 -1)
-                      (1 3 4 -2)
-                      (2 2 4  0)
-                      (2 3 5 -1)))))
-
-  (: tabulate-state*+headers
-     (All (a) (-> (Listof (-> (State a) a)) (DomainMapping a)
-                  (Pairof (Listof Symbol) (Listof (Listof a))))))
-  (define (tabulate-state*+headers funcs domains)
-    (define var-names : (Listof Symbol)
-      (hash-map domains (λ ([x : Symbol] _) x) #t))
-    (define func-names : (Listof Symbol)
-      (for/list ([_ funcs]
-                 [i (in-naturals 1)])
-        (string->symbol (~a 'f i))))
-    (cons (append var-names func-names)
-          (tabulate-state* funcs domains)))
-
-  (module+ test
-    (test-case "tabulate-state*+headers"
-      (define/: f1 (State Integer) (+ :a :b))
-      (define/: f2 (State Integer) (- :a :b))
-      (check-equal?
-       (tabulate-state*+headers (list f1 f2) (hash 'a '(1 2) 'b '(2 3)))
-       '((a b f1 f2)
-         (1 2 3 -1)
-         (1 3 4 -2)
-         (2 2 4 0)
-         (2 3 5 -1)))))
-
-  (: tabulate-state*/boolean
-     (-> (Listof (-> (State Boolean) Boolean)) (Listof Variable)
-         (Listof (Listof Boolean))))
-  (define (tabulate-state*/boolean funcs args)
-    (tabulate-state* funcs (make-boolean-domains args)))
-
-  (module+ test
-    (test-case "tabulate-state*/boolean"
-      (define/: f1 (State Boolean) (and :a :b))
-      (define/: f2 (State Boolean) (or :a :b))
-      (check-equal? (tabulate-state*/boolean (list f1 f2) '(a b))
-                    '((#f #f #f #f)
-                      (#f #t #f #t)
-                      (#t #f #f #t)
-                      (#t #t #t #t)))))
-
-  (: tabulate-state*+headers/boolean
-     (-> (Listof (-> (State Boolean) Boolean)) (Listof Variable)
-         (Pairof (Listof Symbol) (Listof (Listof Boolean)))))
-  (define (tabulate-state*+headers/boolean funcs args)
-    (tabulate-state*+headers funcs (make-boolean-domains args)))
-
-  (module+ test
-    (test-case "tabulate-state*+headers/boolean"
-      (define/: f1 (State Boolean) (and :a :b))
-      (define/: f2 (State Boolean) (or :a :b))
-      (check-equal? (tabulate-state*+headers/boolean (list f1 f2) '(a b))
-                    '((a b f1 f2)
-                      (#f #f #f #f)
-                      (#f #t #f #t)
-                      (#t #f #f #t)
-                      (#t #t #t #t)))))
-
-  (define-syntax-parse-rule (make-tabulate-no-star name star-name)
-    (define (name func domains)
-      (star-name `(,func) domains)))
-
-  (: tabulate-state (All (a) (-> (-> (State a) a) (DomainMapping a)
-                                 (Listof (Listof a)))))
-  (make-tabulate-no-star tabulate-state tabulate-state*)
-
-  (module+ test
-    (test-case "tabulate-state"
-      (check-equal? (tabulate-state (λ/: (State Integer) (+ :a :b))
-                                    (hash 'a '(1 2) 'b '(2 3)))
-                    '((1 2 3)
-                      (1 3 4)
-                      (2 2 4)
-                      (2 3 5)))))
-
-  (: tabulate-state+headers (All (a) (-> (-> (State a) a) (DomainMapping a)
-                                         (Pairof (Listof Symbol)
-                                                 (Listof (Listof a))))))
-  (make-tabulate-no-star tabulate-state+headers tabulate-state*+headers)
-
-  (module+ test
-    (test-case "tabulate-state+headers"
-      (check-equal? (tabulate-state+headers
-                     (λ/: (State Integer) (+ :a :b))
-                     (hash 'a '(1 2) 'b '(2 3)))
-                    '((a b f1)
-                      (1 2 3)
-                      (1 3 4)
-                      (2 2 4)
-                      (2 3 5)))))
-
-  (: tabulate-state/boolean
-     (-> (-> (State Boolean) Boolean)
-         (Listof Variable)
-         (Listof (Listof Boolean))))
-  (make-tabulate-no-star tabulate-state/boolean tabulate-state*/boolean)
-
-  (module+ test
-    (test-case "tabulate-state/boolean"
-      (check-equal? (tabulate-state/boolean (λ/: (State Boolean) (and :a :b)) '(a b))
-                    '((#f #f #f)
-                      (#f #t #f)
-                      (#t #f #f)
-                      (#t #t #t)))))
-
-  (: tabulate-state+headers/boolean
-     (-> (-> (State Boolean) Boolean)
-         (Listof Variable)
-         (Pairof (Listof Symbol) (Listof (Listof Boolean)))))
-  (make-tabulate-no-star tabulate-state+headers/boolean tabulate-state*+headers/boolean)
-
-  (module+ test
-    (test-case "tabulate-state+headers/boolean"
-      (check-equal? (tabulate-state+headers/boolean
-                     (λ/: (State Boolean) (and :a :b)) '(a b))
-                    '((a b f1)
-                      (#f #f #f)
-                      (#f #t #f)
-                      (#t #f #f)
-                      (#t #t #t)))))
-
-  (: tabulate-network (All (a) (-> (Network a) (Listof (Listof a)))))
-  (define (tabulate-network network)
-    (define funcs (hash-map (network-functions network)
-                            (λ (_ [fx : (UpdateFunction a)]) fx)
-                            #t))
-    (tabulate-state* funcs (network-domains network)))
-
-  (module+ test
-    (test-case "tabulate-network"
-      (define bn (forms->boolean-network (hash 'a '(not a) 'b 'b)))
-      (check-equal? (tabulate-network bn)
-                    '((#f #f #t #f)
-                      (#f #t #t #t)
-                      (#t #f #f #f)
-                      (#t #t #f #t)))))
-
-  (: tabulate-network+headers (All (a) (-> (Network a)
-                                           (Pairof (Listof Symbol)
-                                                   (Listof (Listof a))))))
-  (define (tabulate-network+headers network)
-    (define-values (vars funcs)
-      (for/lists ([l1 : (Listof Variable)]
-                  [l2 : (Listof (UpdateFunction a))])
-                 ([p (hash-map (network-functions network)
-                               (inst cons Variable (UpdateFunction a))
-                               #t)])
-        (values (car p) (cdr p))))
-
-    (define fnames : (Listof Variable)
-      (for/list ([v vars]) (format-symbol "f-~a" v)))
-
-    (match (tabulate-state*+headers funcs (network-domains network))
-      [(list headers tab ...)
-       (cons (append (take headers (length fnames)) fnames)
-             tab)]))
-
-  (module+ test
-    (test-case "tabulate-network+headers"
-      (define bn (forms->boolean-network (hash 'a '(not a) 'b 'b)))
-      (check-equal? (tabulate-network+headers bn)
-                    '((a b f-a f-b)
-                      (#f #f #t #f)
-                      (#f #t #t #t)
-                      (#t #f #f #f)
-                      (#t #t #f #t)))))
-
-  (: table+vars->network (All (a) (-> (Listof Variable) (Listof (Listof a))
-                                      (Network a))))
-  (define (table+vars->network var-names table)
-    (define n : Integer (quotient (length (car table)) 2))
-    ;; Split the table into the inputs and the outputs of the functions.
-    (define-values (ins outs) (multi-split-at table n))
-    ;; Transpose outs to have functions define by lines instead of by
-    ;; columns.
-    (define func-lines : (Listof (Listof a)) (lists-transpose outs))
-    ;; Make states out of inputs.
-    (define st-ins : (Listof (State a))
-      (for/list ([in ins]) (make-immutable-hash
-                            (map (inst cons Variable a) var-names in))))
-    ;; Construct the functions.
-    (define funcs : (Listof (UpdateFunction a))
-      (for/list ([out func-lines])
-        (table->unary-function
-         (for/list : (Listof (List (State a) a))
-                   ([in st-ins] [o out])
-           (list in o)))))
-    ;; Infer the domains.
-    (define domains : (DomainMapping a)
-      (make-immutable-hash
-       (map (inst cons Variable (Domain a))
-            var-names
-            (map (inst remove-duplicates a) (lists-transpose ins)))))
-    ;; Construct the network.
-    (network (make-immutable-hash
-              (map (inst cons Variable (UpdateFunction a))
-                   var-names funcs))
-             domains))
-
-  (module+ test
-    (test-case "table+vars->network"
-      (define n (table+vars->network '(x1 x2)
-                                     '((#f #f #f #f)
-                                       (#f #t #f #t)
-                                       (#t #f #t #f)
-                                       (#t #t #t #t))))
-      (define f1 (hash-ref (network-functions n) 'x1))
-      (define f2 (hash-ref (network-functions n) 'x2))
-
-      (check-false (f1 (hash 'x1 #f 'x2 #f)))
-      (check-false (f1 (hash 'x1 #f 'x2 #t)))
-      (check-true (f1 (hash 'x1 #t 'x2 #f)))
-      (check-true (f1 (hash 'x1 #t 'x2 #t)))
-
-      (check-false (f2 (hash 'x1 #f 'x2 #f)))
-      (check-true (f2 (hash 'x1 #f 'x2 #t)))
-      (check-false (f2 (hash 'x1 #t 'x2 #f)))
-      (check-true (f2 (hash 'x1 #t 'x2 #t)))
-
-      (check-equal? (network-domains n)
-                    #hash((x1 . (#f #t)) (x2 . (#f #t))))))
-
-  (: table->network (All (a) (-> (Listof (Listof a)) (Network a))))
-  (define (table->network table)
-    (define n : Integer (quotient (length (car table)) 2))
-    (define var-names : (Listof Variable)
-      (for/list : (Listof Variable)
-                ([i (in-range 1 (add1 n))])
-        (format-symbol "x~a" i)))
-    (table+vars->network var-names table))
-
-  (module+ test
-    (test-case "table->network"
-      (define n (table->network '((#f #f #f #f)
-                                  (#f #t #f #t)
-                                  (#t #f #t #f)
-                                  (#t #t #t #t))))
-      (define f1 (hash-ref (network-functions n) 'x1))
-      (define f2 (hash-ref (network-functions n) 'x2))
-
-      (check-false (f1 (hash 'x1 #f 'x2 #f)))
-      (check-false (f1 (hash 'x1 #f 'x2 #t)))
-      (check-true (f1 (hash 'x1 #t 'x2 #f)))
-      (check-true (f1 (hash 'x1 #t 'x2 #t)))
-
-      (check-false (f2 (hash 'x1 #f 'x2 #f)))
-      (check-true (f2 (hash 'x1 #f 'x2 #t)))
-      (check-false (f2 (hash 'x1 #t 'x2 #f)))
-      (check-true (f2 (hash 'x1 #t 'x2 #t)))
-
-      (check-equal? (network-domains n)
-                    #hash((x1 . (#f #t)) (x2 . (#f #t))))))
-
-  (: table+headers->network (All (a) (-> (Pairof (Listof Symbol) (Listof (Listof a)))
-                                         (Network a))))
-  (define (table+headers->network table)
-    (define headers : (Listof Symbol) (car table))
-    (define var-names : (Listof Variable)
-      (drop-right headers (quotient (length headers) 2)))
-    (table+vars->network var-names (cdr table)))
-
-  (module+ test
-    (test-case "table+headers->network"
-      (define n (table+headers->network
-                 '((x1 x2 f1 f2)
-                   (#f #f #f #f)
-                   (#f #t #f #t)
-                   (#t #f #t #f)
-                   (#t #t #t #t))))
-      (define f1 (hash-ref (network-functions n) 'x1))
-      (define f2 (hash-ref (network-functions n) 'x2))
-
-      (check-false (f1 (hash 'x1 #f 'x2 #f)))
-      (check-false (f1 (hash 'x1 #f 'x2 #t)))
-      (check-true (f1 (hash 'x1 #t 'x2 #f)))
-      (check-true (f1 (hash 'x1 #t 'x2 #t)))
-
-      (check-false (f2 (hash 'x1 #f 'x2 #f)))
-      (check-true (f2 (hash 'x1 #f 'x2 #t)))
-      (check-false (f2 (hash 'x1 #t 'x2 #f)))
-      (check-true (f2 (hash 'x1 #t 'x2 #t)))
-
-      (check-equal? (network-domains n)
-                    #hash((x1 . (#f #t)) (x2 . (#f #t))))))
-
-  (: random-function/state (All (a) (-> (DomainMapping a) (Domain a)
-                                        (-> (State a) a))))
-  (define (random-function/state arg-domains func-domain)
-    (table->unary-function
-     (for/list : (Listof (List (State a) a))
-               ([st (build-all-states arg-domains)])
-       (list st (random-ref func-domain)))))
-
-  (module+ test (random-seed 1))
-
-  (module+ test
-    (test-case "random-function/state"
-      (define doms (hash 'a '(1 2) 'b '(3 4)))
-      (define f (random-function/state doms '(e f)))
-      (check-equal? (tabulate-state+headers f doms)
-                    '((a b f1) (1 3 e) (1 4 e) (2 3 f) (2 4 e)))))
-
-  (: random-boolean-function/state (-> (Listof Variable) (-> (State Boolean) Boolean)))
-  (define (random-boolean-function/state args)
-    (random-function/state (make-boolean-domains args) '(#f #t)))
-
-  (module+ test
-    (test-case "random-boolean-function/state"
-      (define f (random-boolean-function/state '(x1 x2)))
-      (check-equal? (tabulate-state+headers/boolean f '(x1 x2))
-                    '((x1 x2 f1) (#f #f #f) (#f #t #f) (#t #f #t) (#t #t #t)))))
-
-  (: random-network (All (a) (-> (DomainMapping a) (Network a))))
-  (define (random-network domains)
-    (network (for/hash : (VariableMapping (UpdateFunction a))
-                 ([(x x-dom) (in-hash domains)])
-               (values x (random-function/state domains x-dom)))
-             domains))
-
-  (module+ test
-    (test-case "random-network"
-      (check-equal?
-       (tabulate-network+headers (random-network (hash 'a '(1 2) 'b '(#f #t))))
-       '((a b f-a f-b) (1 #f 1 #f) (1 #t 1 #f) (2 #f 2 #t) (2 #t 2 #f)))))
-
-  (: random-boolean-network (-> (Listof Variable) (Network Boolean)))
-  (define (random-boolean-network vars)
-    (random-network (make-boolean-domains vars)))
-
-  (module+ test
-    (test-case "random-boolean-network"
-      (check-equal?
-       (tabulate-network+headers (random-boolean-network '(x y z)))
-       '((x y z f-x f-y f-z)
-         (#f #f #f #t #t #t)
-         (#f #f #t #f #f #f)
-         (#f #t #f #t #t #t)
-         (#f #t #t #f #t #f)
-         (#t #f #f #t #t #t)
-         (#t #f #t #f #t #f)
-         (#t #t #f #f #f #t)
-         (#t #t #t #t #t #f)))))
-
-  (: random-boolean-network/n (-> Positive-Integer (Network Boolean)))
-  (define (random-boolean-network/n n)
-    (random-boolean-network (for/list : (Listof Variable)
-                                      ([i (in-range n)])
-                              (string->symbol (format "x~a" i)))))
-
-  (module+ test
-    (test-case "random-boolean-network/n"
-      (check-equal?
-       (tabulate-network+headers (random-boolean-network/n 3))
-       '((x0 x1 x2 f-x0 f-x1 f-x2)
-         (#f #f #f #f #t #f)
-         (#f #f #t #f #f #t)
-         (#f #t #f #t #f #f)
-         (#f #t #t #f #t #t)
-         (#t #f #f #t #t #t)
-         (#t #f #t #t #f #t)
-         (#t #t #f #t #t #f)
-         (#t #t #t #t #f #t)))))
-  )
-
-(require 'typed)
-
-
-(require (except-in "utils.rkt" lists-transpose) (submod "utils.rkt" untyped)
-         "generic.rkt" "functions.rkt"
-         graph racket/random racket/hash)
-
-(provide
- ;; Structures
- (contract-out [struct tbf/state ([weights (hash/c variable? number?)]
-                                  [threshold number?])]
-               [struct dynamics ([network network?]
-                                 [mode mode?])])
- ;; Functions
- (contract-out [build-signed-interaction-graph (-> network? graph?)]
-               [build-signed-interaction-graph/form (-> network-form? graph?)]
-               [make-asyn (-> (listof variable?) mode?)]
-               [make-syn (-> (listof variable?) mode?)]
-               [make-dynamics-from-func (-> network? (-> (listof variable?) mode?) dynamics?)]
-               [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?))]
-               [dds-build-state-graph (-> dynamics? (set/c state? #:kind 'dont-care) graph?)]
-               [dds-build-n-step-state-graph (-> dynamics? (set/c state? #:kind 'dont-care) number? graph?)]
-               [dds-build-state-graph-annotated (-> dynamics? (set/c state? #:kind 'dont-care) graph?)]
-               [dds-build-n-step-state-graph-annotated (-> dynamics? (set/c state? #:kind 'dont-care) number? graph?)]
-               [pretty-print-state (-> state? string?)]
-               [pretty-print-boolean-state (-> state? string?)]
-               [pretty-print-state-graph-with (-> graph? (-> state? string?) graph?)]
-               [pretty-print-state-graph (-> graph? graph?)]
-               [ppsg (-> graph? graph?)]
-               [pretty-print-boolean-state-graph (-> graph? graph?)]
-               [ppsgb (-> graph? graph?)]
-               [build-full-state-graph (-> dynamics? graph?)]
-               [build-full-state-graph-annotated (-> dynamics? graph?)]
-               [tabulate-state (->* (procedure? domain-mapping/c) (#:headers boolean?)
-                                    (listof (listof any/c)))]
-               [tabulate-state* (->* ((non-empty-listof procedure?) domain-mapping/c) (#:headers boolean?)
-                                     (listof (listof any/c)))]
-               [tabulate-state/boolean (->* (procedure? (listof variable?)) (#:headers boolean?)
-                                            (listof (listof any/c)))]
-               [tabulate-state*/boolean (->* ((non-empty-listof procedure?) (listof variable?)) (#:headers boolean?)
-                                             (listof (listof any/c)))]
-               [tabulate-network (->* (network?) (#:headers boolean?)
-                                      (listof (listof any/c)))]
-               [table->network (->* ((listof (*list/c any/c any/c))) (#:headers boolean?) network?)]
-               [random-function/state (domain-mapping/c generic-set? . -> . procedure?)]
-               [random-boolean-function/state ((listof variable?) . -> . procedure?)]
-               [random-network (domain-mapping/c . -> . network?)]
-               [random-boolean-network ((listof variable?) . -> . network?)]
-               [random-boolean-network/vars (number? . -> . network?)]
-               [apply-tbf-to-state (-> tbf? state? (or/c 0 1))]
-               [tbf/state-w (-> tbf/state? (hash/c variable? number?))]
-               [tbf/state-θ (-> tbf/state? number?)]
-               [make-tbf/state (-> (listof (cons/c variable? number?)) number? tbf/state?)]
-               [make-sbf/state (-> (listof (cons/c variable? number?)) sbf/state?)]
-               [apply-tbf/state (-> tbf/state? (hash/c variable? (or/c 0 1)) (or/c 0 1))]
-               [lists->tbfs/state (->* ((listof (listof (or/c number? symbol?))))
-                                       (#:headers boolean?)
-                                       (listof tbf/state?))]
-               [lists->sbfs/state (->* ((listof (listof (or/c number? symbol?))))
-                                       (#:headers boolean?)
-                                       (listof sbf/state?))]
-               [read-org-tbfs/state (->* (string?) (#:headers boolean?) (listof tbf/state?))]
-               [read-org-sbfs/state (->* (string?) (#:headers boolean?) (listof sbf/state?))]
-               [print-org-tbfs/state (->* ((non-empty-listof tbf/state?)) (#:headers boolean?)
-                                          (listof (listof (or/c number? symbol?))))]
-               [print-org-sbfs/state (->* ((non-empty-listof tbf/state?)) (#:headers boolean?)
-                                          (listof (listof (or/c number? symbol?))))]
-               [tbf/state-tabulate* (->* ((non-empty-listof tbf/state?)) (#:headers boolean?)
-                                         (listof (listof (or/c symbol? number?))))]
-               [tbf/state-tabulate (->* (tbf/state?) (#:headers boolean?)
-                                        (listof (listof (or/c symbol? number?))))]
-               [group-truth-table-by-nai (-> (listof (listof (or/c 0 1))) (listof (listof (listof (or/c 0 1)))))]
-               [make-tbn (-> (listof (cons/c variable? tbf/state?)) tbn?)]
-               [tbn->network (-> tbn? network?)]
-               [make-sbn (-> (listof (cons/c variable? tbf/state?)) sbn?)]
-               [parse-org-tbn (->* ((listof any/c))
-                                   (#:headers boolean? #:func-names boolean?)
-                                   tbn?)]
-               [read-org-tbn (->* (string?)
-                                  (#:headers boolean? #:func-names boolean?)
-                                  tbn?)]
-               [read-org-sbn (->* (string?)
-                                  (#:headers boolean? #:func-names boolean?)
-                                  tbn?)]
-               [build-tbn-state-graph (-> tbn? graph?)]
-               [normalized-tbn? (-> tbn? boolean?)]
-               [normalize-tbn (-> tbn? normalized-tbn?)]
-               [compact-tbf (-> tbf/state? tbf/state?)]
-               [compact-tbn (-> tbn? tbn?)]
-               [print-org-tbn (->* (tbn?) (#:headers boolean? #:func-names boolean?)
-                                   (listof (listof (or/c number? symbol?))))]
-               [print-org-sbn (->* (sbn?) (#:headers boolean? #:func-names boolean?)
-                                   (listof (listof (or/c number? symbol?))))]
-               [tbn-interaction-graph (->* (tbn?) (#:zero-edges boolean?)
-                                           graph?)]
-               [pretty-print-tbn-interaction-graph (-> graph? graph?)]
-               [sbn-interaction-graph (->* (sbn?) (#:zero-edges boolean?)
-                                           graph?)])
- ;; Predicates
- (contract-out [variable? (-> any/c boolean?)]
-               [state? (-> any/c boolean?)]
-               [update-function-form? (-> any/c boolean?)]
-               [modality? (-> any/c boolean?)]
-               [mode? (-> any/c boolean?)]
-               [sbf/state? (-> any/c boolean?)])
- ;; Contracts
- (contract-out [state/c contract?]
-               [update-function/c contract?]
-               [domain-mapping/c contract?]
-               [tbn? contract?]
-               [sbn? contract?]))
+(require "utils.rkt" "functions.rkt" "dynamics.rkt"
+         typed/graph typed/racket/random
+         syntax/parse/define)
+(require/typed racket/syntax
+  [format-symbol (-> String Any * Symbol)])
 
 (module+ test
-  (require rackunit)
-  ;; When this variable is set to #t, some particularly expensive test
-  ;; cases are omitted.
+  (require typed/rackunit)
   (define skip-expensive-tests? #t)
   (unless skip-expensive-tests?
     (displayln "Running the complete test suite...")))
 
+(provide
+ State UpdateFunction Domain DomainMapping
+ 01->boolean/state
 
-;;; =================
-;;; Basic definitions
-;;; =================
+ (struct-out network) Network
+ make-same-domains make-boolean-domains make-boolean-network
+ make-01-domains make-01-network update
 
-(define variable? symbol?)
+ UpdateFunctionForm (struct-out network-form) NetworkForm
+ update-function-form->update-function/any
+ update-function-form->update-function/boolean
+ update-function-form->update-function/01
+ network-form->network/any network-form->network/boolean
+ network-form->network/01 make-boolean-network-form
+ forms->boolean-network
 
-;;; A state of a network is a mapping from the variables of the
-;;; network to their values.
-(define state? variable-mapping?)
-(define state/c (flat-named-contract 'state state?))
+ build-all-states build-all-boolean-states build-all-01-states
 
-;;; An update function is a function computing a value from the given
-;;; state.
-(define update-function/c (-> state? any/c))
+ list-syntactic-interactions build-syntactic-interaction-graph
+ interaction? get-interaction-sign build-interaction-graph
+ build-interaction-graph/form build-signed-interaction-graph
+ build-signed-interaction-graph/form
 
-;;; A domain mapping is a hash set mapping variables to the lists of
-;;; values in their domains.
-(define domain-mapping/c (hash/c variable? list?))
+ Modality Mode dynamics% Dynamics% make-syn make-asyn
+ make-asyn-dynamics make-syn-dynamics build-full-state-graph
+ build-full-state-graph/annotated
+ pretty-print-state pretty-print-state/01 pretty-print-state-graph-with
+ pretty-print-state-graph ppsg pretty-print-state-graph/01 ppsg01
 
+ tabulate-state* tabulate-state*/boolean
+ tabulate-state*+headers tabulate-state*+headers/boolean
+ tabulate-state tabulate-state/boolean
+ tabulate-state+headers tabulate-state+headers/boolean
+ tabulate-network tabulate-network+headers
 
-;;; =================================
-;;; Syntactic description of networks
-;;; =================================
+ table+vars->network table->network table+headers->network
 
-(define update-function-form? any/c)
+ random-function/state random-boolean-function/state random-network
+ random-boolean-network random-boolean-network/n
+ )
 
+(define-type (State a) (VariableMapping a))
+(define-type (UpdateFunction a) (-> (State a) a))
+(define-type (Domain a) (Listof a))
+(define-type (DomainMapping a) (VariableMapping (Domain a)))
 
-;;; ====================
-;;; Dynamics of networks
-;;; ====================
-
-(define modality? (set/c variable?))
-(define mode? (set/c modality?))
-
-;;; A network dynamics is a network plus a mode.
-(struct dynamics (network mode)
-  #:methods gen:dds
-  [;; 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).
-(define (make-asyn vars)
-  (for/set ([v vars]) (set v)))
-
-;;; Given a list of variables, builds the synchronous mode (a set
-;;; containing the set of variables).
-(define (make-syn vars) (set (list->set vars)))
+(: 01->boolean/state (-> (State (U Zero One)) (State Boolean)))
+(define (01->boolean/state s)
+  (for/hash ([(x val) (in-hash s)]) : (State Boolean)
+            (if (eq? val 1) (values x #t) (values x #f))))
 
 (module+ test
-  (test-case "make-asyn, make-syn"
-    (define vars '(a b c))
-    (check-equal? (make-asyn vars) (set (set 'a) (set 'b) (set 'c)))
-    (check-equal? (make-syn vars) (set (set 'a 'b 'c)))))
+  (test-case "01->boolean/state"
+    (check-equal? (01->boolean/state (hash 'a 0 'b 1))
+                  (hash 'a #f 'b #t))))
+
+(struct (a) network ([functions : (VariableMapping (UpdateFunction a))]
+                     [domains : (DomainMapping a)])
+  #:transparent
+  #:type-name Network)
+
+(: make-same-domains (All (a) (-> (Listof Variable) (Domain a)
+                                  (DomainMapping a))))
+(define (make-same-domains vars domain)
+  (for/hash ([var vars]) : (DomainMapping a)
+            (values var domain)))
+
+(module+ test
+  (test-case "make-same-domains"
+    (check-equal? (make-same-domains '(a b) '(1 2))
+                  #hash((a . (1 2)) (b . (1 2))))))
+
+(: make-boolean-domains (-> (Listof Variable) (DomainMapping Boolean)))
+(define (make-boolean-domains vars)
+  (make-same-domains vars '(#f #t)))
+
+(module+ test
+  (test-case "make-boolean-domains"
+    (check-equal? (make-boolean-domains '(a b))
+                  #hash((a . (#f #t)) (b . (#f #t))))))
+
+(: make-boolean-network (-> (VariableMapping (UpdateFunction Boolean))
+                            (Network Boolean)))
+(define (make-boolean-network funcs)
+  (network funcs (make-boolean-domains (hash-keys funcs))))
+
+(module+ test
+  (test-case "make-boolean-network"
+    (define f1 (λ ([s : (State Boolean)])
+                 (and (hash-ref s 'x1) (not (hash-ref s 'x2)))))
+    (define f2 (λ ([s : (State Boolean)])
+                 (not (hash-ref s 'x2))))
+    (define bn (make-boolean-network (hash 'x1 f1 'x2 f2)))
+    (check-equal? (network-domains bn) (hash 'x1 '(#f #t) 'x2 '(#f #t)))))
+
+(: make-01-domains (-> (Listof Variable) (DomainMapping (U Zero One))))
+(define (make-01-domains vars)
+  (make-same-domains vars '(0 1)))
+
+(module+ test
+  (test-case "make-01-domains"
+    (check-equal? (make-01-domains '(a b))
+                  '#hash((a . (0 1)) (b . (0 1))))))
+
+(: make-01-network (-> (VariableMapping (UpdateFunction (U Zero One)))
+                       (Network (U Zero One))))
+(define (make-01-network funcs)
+  (network funcs (make-01-domains (hash-keys funcs))))
+
+(module+ test
+  (test-case "make-01-network"
+    (define f1 (λ ([s : (State (U Zero One))])
+                 (assert-type (max (hash-ref s 'a) (hash-ref s 'b))
+                              (U Zero One))))
+    (define f2 (λ ([s : (State (U Zero One))])
+                 (assert-type (min (hash-ref s 'a) (hash-ref s 'b))
+                              (U Zero One))))
+    (define n (make-01-network (hash 'a f1 'b f2)))
+    (check-equal? (network-domains n) (hash 'a '(0 1) 'b '(0 1)))))
+
+(: update (All (a) (-> (Network a) (State a) (Listof Variable) (State a))))
+(define (update network s xs)
+  (define funcs (network-functions network))
+  (for/fold ([new-s : (State a) s])
+            ([x xs])
+    (define fx (hash-ref funcs x))
+    (hash-set new-s x (fx s))))
+
+(module+ test
+  (test-case "update"
+    (define f1 (λ ([s : (State Boolean)])
+                 (and (hash-ref s 'x1) (not (hash-ref s 'x2)))))
+    (define f2 (λ ([s : (State Boolean)])
+                 (not (hash-ref s 'x2))))
+    (define bn (make-boolean-network (hash 'x1 f1 'x2 f2)))
+    (check-equal? (update bn (hash 'x1 #f 'x2 #f) '(x1))
+                  #hash((x1 . #f) (x2 . #f)))
+    (check-equal? (update bn (hash 'x1 #f 'x2 #f) '(x1 x2))
+                  #hash((x1 . #f) (x2 . #t)))))
+
+(define-type UpdateFunctionForm Any)
+
+(struct (a) network-form ([forms : (VariableMapping UpdateFunctionForm)]
+                          [domains : (DomainMapping a)])
+  #:transparent
+  #:type-name NetworkForm)
+
+(: update-function-form->update-function/any (-> UpdateFunctionForm (UpdateFunction Any)))
+(define (update-function-form->update-function/any form)
+  (λ (s) (eval1-with s form)))
+
+(module+ test
+  (test-case "update-function-form->update-function/any"
+    (define s (hash 'x #t 'y #f))
+    (define f (update-function-form->update-function/any '(and x y)))
+    (check-equal? (f s) #f)))
+
+(: update-function-form->update-function/boolean (-> UpdateFunctionForm (UpdateFunction Boolean)))
+(define (update-function-form->update-function/boolean form)
+  (λ (s) (assert-type (eval1-with s form) Boolean)))
+
+(module+ test
+  (test-case "update-function-form->update-function/boolean"
+    (define s (hash 'x #t 'y #f))
+    (define f (update-function-form->update-function/boolean '(and x y)))
+    (check-equal? (f s) #f)))
+
+(: update-function-form->update-function/01 (-> UpdateFunctionForm (UpdateFunction (U Zero One))))
+(define (update-function-form->update-function/01 form)
+  (λ (s) (assert-type (eval1-with s form) (U Zero One))))
+
+(module+ test
+  (test-case "update-function-form->update-function/01"
+    (define s (hash 'x 0 'y 1))
+    (define f (update-function-form->update-function/01 '(max x y)))
+    (check-equal? (f s) 1)))
+
+(: network-form->network/any (-> (NetworkForm Any) (Network Any)))
+(define (network-form->network/any nf)
+  (network
+   (for/hash ([(x form) (in-hash (network-form-forms nf))])
+     : (VariableMapping (UpdateFunction Any))
+     (values x (update-function-form->update-function/any form)))
+   (network-form-domains nf)))
+
+(module+ test
+  (test-case "network-form->network/any"
+    (define bn (network-form->network/any
+                (network-form (hash 'a '(and a b)
+                                    'b '(not b))
+                              (hash 'a '(#f #t)
+                                    'b '(#f #t)))))
+    (define s (hash 'a #t 'b #t))
+    (check-equal? ((hash-ref (network-functions bn) 'a) s) #t)))
+
+(: network-form->network/boolean (-> (NetworkForm Boolean) (Network Boolean)))
+(define (network-form->network/boolean nf)
+  (network
+   (for/hash ([(x form) (in-hash (network-form-forms nf))])
+     : (VariableMapping (UpdateFunction Boolean))
+     (values x (update-function-form->update-function/boolean form)))
+   (network-form-domains nf)))
+
+(module+ test
+  (test-case "network-form->network/boolean"
+    (define bn (network-form->network/boolean
+                (network-form (hash 'a '(and a b)
+                                    'b '(not b))
+                              (hash 'a '(#f #t)
+                                    'b '(#f #t)))))
+    (define s (hash 'a #t 'b #t))
+    (check-equal? ((hash-ref (network-functions bn) 'a) s) #t)))
+
+(: network-form->network/01 (-> (NetworkForm (U Zero One)) (Network (U Zero One))))
+(define (network-form->network/01 nf)
+  (network
+   (for/hash ([(x form) (in-hash (network-form-forms nf))])
+     : (VariableMapping (UpdateFunction (U Zero One)))
+     (values x (update-function-form->update-function/01 form)))
+   (network-form-domains nf)))
+
+(module+ test
+  (test-case "network-form->network/01"
+    (define bn (network-form->network/01
+                (network-form (hash 'a '(min a b)
+                                    'b '(- 1 b))
+                              (hash 'a '(0 1)
+                                    'b '(0 1)))))
+    (define s (hash 'a 1 'b 1))
+    (check-equal? ((hash-ref (network-functions bn) 'a) s) 1)))
+
+(: make-boolean-network-form (-> (VariableMapping UpdateFunctionForm)
+                                 (NetworkForm Boolean)))
+(define (make-boolean-network-form forms)
+  (network-form forms (make-boolean-domains (hash-keys forms))))
+
+(module+ test
+  (test-case "make-boolean-network-form"
+    (check-equal? (make-boolean-network-form (hash 'a '(and a b)
+                                                   'b '(not b)))
+                  (network-form
+                   '#hash((a . (and a b)) (b . (not b)))
+                   '#hash((a . (#f #t)) (b . (#f #t)))))))
+
+(: forms->boolean-network (-> (VariableMapping UpdateFunctionForm)
+                              (Network Boolean)))
+(define forms->boolean-network
+  (compose network-form->network/boolean make-boolean-network-form))
+
+(module+ test
+  (test-case "forms->boolean-network"
+    (define n (forms->boolean-network (hash 'a '(and a b)
+                                            'b '(not b))))
+    (check-equal? (network-domains n) (hash 'a '(#f #t)
+                                            'b '(#f #t)))))
+
+(: build-all-states (All (a) (-> (DomainMapping a) (Listof (State a)))))
+(define (build-all-states vars-domains)
+  ;; TODO: Use hash-keys and hash-values when Typed Racket will have
+  ;; caught up with the new argument try-order?.
+  (define vdlist (hash-map vars-domains (inst cons Variable (Domain a)) #t))
+  (define vars (map (inst car Variable (Domain a)) vdlist))
+  (define doms (map (inst cdr Variable (Domain a)) vdlist))
+  (for/list ([s (apply cartesian-product doms)])
+    (make-immutable-hash (map (inst cons Variable a) vars s))))
+
+(module+ test
+  (test-case "build-all-states"
+    (check-equal? (build-all-states #hash((a . (#t #f)) (b . (1 2 3))))
+                  '(#hash((a . #t) (b . 1))
+                    #hash((a . #t) (b . 2))
+                    #hash((a . #t) (b . 3))
+                    #hash((a . #f) (b . 1))
+                    #hash((a . #f) (b . 2))
+                    #hash((a . #f) (b . 3))))))
+
+(: build-all-boolean-states (-> (Listof Variable) (Listof (State Boolean))))
+(define (build-all-boolean-states vars)
+  (build-all-states (make-boolean-domains vars)))
+
+(module+ test
+  (test-case "build-all-boolean-states"
+    (check-equal? (build-all-boolean-states '(a b))
+                  '(#hash((a . #f) (b . #f))
+                    #hash((a . #f) (b . #t))
+                    #hash((a . #t) (b . #f))
+                    #hash((a . #t) (b . #t))))))
+
+(: build-all-01-states (-> (Listof Variable) (Listof (State (U Zero One)))))
+(define (build-all-01-states vars)
+  (build-all-states (make-01-domains vars)))
+
+(module+ test
+  (test-case "build-all-01-states"
+    (check-equal? (build-all-01-states '(a b))
+                  '(#hash((a . 0) (b . 0))
+                    #hash((a . 0) (b . 1))
+                    #hash((a . 1) (b . 0))
+                    #hash((a . 1) (b . 1))))))
+
+(: list-syntactic-interactions
+   (All (a) (-> (NetworkForm a) Variable (Listof Variable))))
+(define (list-syntactic-interactions nf x)
+  (set-intersect
+   (extract-symbols (hash-ref (network-form-forms nf) x))
+   (hash-keys (network-form-forms nf))))
+
+(module+ test
+  (test-case "list-syntactic-interactions"
+    (define n (make-boolean-network-form #hash((a . (+ a b c))
+                                               (b . (- b c)))))
+    (check-true (set=? (list-syntactic-interactions n 'a) '(a b)))
+    (check-true (set=? (list-syntactic-interactions n 'b) '(b)))))
+
+(: build-syntactic-interaction-graph (All (a) (-> (NetworkForm a) Graph)))
+(define (build-syntactic-interaction-graph n)
+  (transpose
+   (unweighted-graph/adj
+    (for/list ([(var _) (in-hash (network-form-forms n))])
+      (cons var (list-syntactic-interactions n var))))))
+
+(module+ test
+  (test-case "build-syntactic-interaction-graph"
+    (define n (make-boolean-network-form #hash((a . (+ a b c))
+                                               (b . (- b c)))))
+    (define ig (build-syntactic-interaction-graph n))
+    (check-true (has-vertex? ig 'a))
+    (check-true (has-vertex? ig 'b))
+    (check-false (has-vertex? ig 'c))
+    (check-true (has-edge? ig 'a 'a))
+    (check-true (has-edge? ig 'b 'a))
+    (check-true (has-edge? ig 'b 'b))
+    (check-false (has-edge? ig 'c 'b))
+    (check-false (has-edge? ig 'c 'a))))
+
+(: interaction? (All (a) (-> (Network a) Variable Variable Boolean)))
+(define (interaction? network x y)
+  (define doms (network-domains network))
+  (define states-not-x (build-all-states (hash-remove doms x)))
+  (define dom-x (hash-ref doms x))
+  (define y-func (hash-ref (network-functions network) y))
+  (: different-ys-exist? (-> (State a) Boolean))
+  (define (different-ys-exist? st)
+    (define x-states (for/list ([x-val (in-list dom-x)])
+                       : (Listof (State a))
+                       (hash-set st x x-val)))
+    ;; TODO: Replace with for*/first when/if it is fixed.
+    (for*/first/typed : (Option Boolean)
+                      ([st1 : (State a) x-states]
+                       [st2 : (State a) x-states]
+                       #:unless (equal? (hash-ref st1 x) (hash-ref st2 x))
+                       #:unless (equal? (y-func st1) (y-func st2)))
+      #t))
+  ;; TODO: Replace with for/first when/if it is fixed.
+  (for/first/typed : (Option Boolean)
+                   ([st (in-list states-not-x)]
+                    #:when (different-ys-exist? st))
+    #t))
+
+(module+ test
+  (test-case "interaction?"
+    (define n1 (forms->boolean-network
+                (hash 'x '(not y)
+                      'y 'x
+                      'z '(and y z))))
+    (check-true (interaction? n1 'x 'y))
+    (check-true (interaction? n1 'y 'x))
+    (check-false (interaction? n1 'x 'z))
+    (define n-multi (hash 'x '(max (+ y 1) 2)
+                          'y '(min (- y 1) 0)))
+    (define 123-doms (make-same-domains '(x y) '(0 1 2)))
+    (define n2 (network-form->network/any (network-form n-multi 123-doms)))
+    (check-false (interaction? n2 'x 'y))
+    (check-true (interaction? n2 'y 'x))))
+
+(: get-interaction-sign (All (a) (-> (Network a) Variable Variable (Option Integer))))
+(define (get-interaction-sign network x y)
+  (define doms (network-domains network))
+  (define dom-x (hash-ref doms x))
+  (define dom-y (hash-ref doms y))
+  (define y-func (hash-ref (network-functions network) y))
+  (define (collect-impacts-on-y [st : (State a)])
+    ;; The way in which the values are ordered in the domains gives
+    ;; a total order on these values.  This means that considering
+    ;; pairs of consecutive values of x is sufficient for testing the
+    ;; sign of the interaction.
+    (define x-states (for/list : (Listof (State a))
+                               ([x-val (in-list dom-x)])
+                       (hash-set st x x-val)))
+    (for/list : (Listof (U '< '> '=))
+              ([st1 (in-list x-states)]
+               [st2 (in-list (cdr x-states))])
+      (define y1-idx (assert-type (index-of dom-y (y-func st1)) Index))
+      (define y2-idx (assert-type (index-of dom-y (y-func st2)) Index))
+      (cond
+        [(< y1-idx y2-idx) '<]
+        [(> y1-idx y2-idx) '>]
+        [else '=])))
+  (define states-not-x (build-all-states (hash-remove doms x)))
+  (define interactions
+    (remove-duplicates
+     (for/list : (Listof (U '< '> '= Zero))
+               ([st (in-list states-not-x)])
+       (define impacts (remove-duplicates (collect-impacts-on-y st)))
+       (cond
+         [(and (member '< impacts) (not (member '> impacts))) '<]
+         [(and (member '> impacts) (not (member '< impacts))) '>]
+         [(equal? impacts '(=)) '=]
+         [else 0]))))
+  (cond
+    [(and (member '< interactions) (not (member '> interactions))) 1]
+    [(and (member '> interactions) (not (member '< interactions))) -1]
+    [(equal? interactions '(=)) #f]
+    [else 0]))
+
+(module+ test
+  (test-case "get-interaction-sign"
+    (define n1 (forms->boolean-network
+                (hash 'x '(not y)
+                      'y 'x
+                      'z '(and y z)
+                      't '(or (and (not x) y)
+                              (and x (not y))))))
+    (check-equal? (get-interaction-sign n1 'x 'y) 1)
+    (check-equal? (get-interaction-sign n1 'y 'x) -1)
+    (check-false (get-interaction-sign n1 'x 'z))
+    (check-equal? (get-interaction-sign n1 'y 'z) 1)
+    (check-equal? (get-interaction-sign n1 'x 't) 0)
+    (define n-multi (hash 'x '(min (+ y 1) 2)
+                          'y '(max (- y 1) 0)
+                          'z '(- 2 y)
+                          't '(abs (- y 1))))
+    (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
+    (define n2 (network-form->network/any (network-form n-multi 123-doms)))
+    (check-false (get-interaction-sign n2 'x 'y))
+    (check-equal? (get-interaction-sign n2 'y 'x) 1)
+    (check-equal? (get-interaction-sign n2 'y 'z) -1)
+    (check-equal? (get-interaction-sign n2 'y 't) 0)
+    (check-equal? (get-interaction-sign n2 'y 'y) 1)))
+
+(: build-interaction-graph (All (a) (-> (Network a) Graph)))
+(define (build-interaction-graph network)
+  (define vars (hash-keys (network-functions network)))
+  (unweighted-graph/directed
+   (for*/list : (Listof (List Any Any))
+              ([x (in-list vars)]
+               [y (in-list vars)]
+               #:when (interaction? network x y))
+     (list x y))))
+
+(: build-interaction-graph/form (All (a) (-> (NetworkForm a) Graph)))
+(define (build-interaction-graph/form form)
+  (build-interaction-graph (network-form->network/any form)))
+
+(module+ test
+  (test-case "build-interaction-graph"
+    (cond
+      [skip-expensive-tests?
+       (displayln "Skipping test case build-interaction-graph.")]
+      [else
+       (define n1 (make-boolean-network-form
+                   (hash 'x '(not y)
+                         'y 'x
+                         'z '(and y z)
+                         't '(or (and (not x) y)
+                                 (and x (not y))))))
+       (check-equal? (graphviz (build-interaction-graph/form n1))
+                     "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node3 [];\n\t\tnode2 -> node2 [];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [];\n\t\tnode0 -> node2 [];\n\t\tnode3 -> node1 [];\n\t}\n}\n")
+       (define n-multi (hash 'x '(min (+ y 1) 2)
+                             'y '(max (- y 1) 0)
+                             'z '(- 2 y)
+                             't '(abs (- y 1))))
+       (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
+       (define n2 (network-form n-multi 123-doms))
+       (check-equal? (graphviz (build-interaction-graph/form n2))
+                     "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [];\n\t\tnode0 -> node2 [];\n\t\tnode0 -> node3 [];\n\t}\n}\n")])))
+
+(: build-signed-interaction-graph (All (a) (-> (Network a) Graph)))
+(define (build-signed-interaction-graph network)
+  (define vars (hash-keys (network-functions network)))
+  (weighted-graph/directed
+   (for*/list : (Listof (List Integer Any Any))
+              ([x (in-list vars)]
+               [y (in-list vars)]
+               [sign (in-value (get-interaction-sign network x y))]
+               #:unless (eq? sign #f))
+     (list sign x y))))
+
+(: build-signed-interaction-graph/form (All (a) (-> (NetworkForm a) Graph)))
+(define (build-signed-interaction-graph/form nf)
+  (build-signed-interaction-graph (network-form->network/any nf)))
+
+(module+ test
+  (test-case "build-signed-interaction-graph"
+    (cond
+      [skip-expensive-tests?
+       (displayln "Skipping test case build-signed-interaction-graph.")]
+      [else
+       (define n1 (make-boolean-network-form
+                   (hash 'x '(not y)
+                         'y 'x
+                         'z '(and y z)
+                         't '(or (and (not x) y)
+                                 (and x (not y))))))
+       (check-equal? (graphviz (build-signed-interaction-graph/form n1))
+                     "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode2 -> node2 [label=\"1\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"0\"];\n\t\tnode0 -> node2 [label=\"1\"];\n\t\tnode0 -> node3 [label=\"-1\"];\n\t\tnode3 -> node1 [label=\"0\"];\n\t\tnode3 -> node0 [label=\"1\"];\n\t}\n}\n")
+       (define n-multi (hash 'x '(min (+ y 1) 2)
+                             'y '(max (- y 1) 0)
+                             'z '(- 2 y)
+                             't '(abs (- y 1))))
+       (define 123-doms (make-same-domains '(x y z t) '(0 1 2)))
+       (define n2 (network-form n-multi 123-doms))
+       (check-equal? (graphviz (build-signed-interaction-graph/form n2))
+                     "digraph G {\n\tnode0 [label=\"y\"];\n\tnode1 [label=\"t\"];\n\tnode2 [label=\"z\"];\n\tnode3 [label=\"x\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [label=\"1\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"0\"];\n\t\tnode0 -> node2 [label=\"-1\"];\n\t\tnode0 -> node3 [label=\"1\"];\n\t}\n}\n")])))
+
+(define-type Modality (Listof Variable))
+(define-type Mode (Listof Modality))
+
+(define dynamics%
+  ;; TODO: Fix the parameter of State when Typed Racket supports
+  ;; passing type parameters to the parent.
+  (class (inst dds% (State Any) Modality)
+    #:forall (a)
+    (super-new)
+
+    (init-field [network : (Network a) network]
+                [mode : Mode mode])
+
+    (: step/annotated (-> (State a) (Listof (Pairof Modality (State a)))))
+    (define/override (step/annotated s)
+      (for/list ([m mode])
+        (cons m (update network s m))))))
+
+;; TODO: Find a better way to define the type of the class
+;; dynamics%.
+;;
+;; TODO: Fix the parameter of State when Typed Racket supports
+;; passing type parameters to the parent.
+;;
+;; NOTE: The type appearing when you type dynamics% in the REPL does
+;; not directly type check, probably because of the structure types
+;; which are fully expanded in the REPL.
+(define-type (Dynamics% a)
+  (Instance (Class
+             (init (network (Network a) #:optional)
+                   (mode Mode #:optional))
+             (field (network (Network a))
+                    (mode Mode))
+             (step (-> (State Any) (Listof (State Any))))
+             (step/annotated (-> (State a) (Listof (Pairof Modality (State a)))))
+             (step* (-> (Listof (State Any)) (Listof (State Any))))
+             (build-state-graph (-> (Listof (State Any)) Graph))
+             (build-state-graph/annotated (-> (Listof (State Any)) Graph))
+             (build-state-graph* (-> (Listof (State Any)) (U Positive-Integer 'full) Graph))
+             (build-state-graph*/annotated (-> (Listof (State Any)) (U Positive-Integer 'full) Graph)))))
+
+(module+ test
+  (let* ([n1 : (Network Boolean)
+             (forms->boolean-network (hash 'x '(not y)
+                                           'y 'x
+                                           'z '(and y z)))]
+         [syn : Mode '((x y z))]
+         [asyn : Mode '((x) (y) (z))]
+         [dyn-syn (new (inst dynamics% Boolean) [network n1] [mode syn])]
+         [dyn-asyn (new (inst dynamics% Boolean) [network n1] [mode asyn])]
+         [s1 (hash 'x #f 'y #f 'z #f)]
+         [s2 (hash 'x #t 'y #t 'z #t)])
+    (test-case "dynamics%"
+      (check-equal? (send dyn-syn step/annotated s1)
+                    '(((x y z) . #hash((x . #t) (y . #f) (z . #f)))))
+      (check-equal? (send dyn-asyn step/annotated s1)
+                    '(((x) . #hash((x . #t) (y . #f) (z . #f)))
+                      ((y) . #hash((x . #f) (y . #f) (z . #f)))
+                      ((z) . #hash((x . #f) (y . #f) (z . #f))))))
+
+    (test-case "dynamics%:step"
+      (check-equal? (send dyn-syn step s1)
+                    '(#hash((x . #t) (y . #f) (z . #f))))
+      (check-equal? (send dyn-asyn step s1)
+                    '(#hash((x . #t) (y . #f) (z . #f))
+                      #hash((x . #f) (y . #f) (z . #f))
+                      #hash((x . #f) (y . #f) (z . #f)))))
+    (test-case "dynamics%:step*"
+      (check-equal? (list->set (send dyn-syn step* (list s1 s2)))
+                    (list->set (append (send dyn-syn step s1)
+                                       (send dyn-syn step s2))))
+      (check-equal? (list->set (send dyn-asyn step* (list s1 s2)))
+                    (list->set (append (send dyn-asyn step s1)
+                                       (send dyn-asyn step s2)))))
+    (test-case "dynamics%:build-state-graph*/annotated"
+      (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 2))
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"'(x y z)\"];\n\t\tnode2 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
+      (check-equal? (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 'full))
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [label=\"'(x y z)\"];\n\t\tnode1 -> node3 [label=\"'(x y z)\"];\n\t\tnode2 -> node1 [label=\"'(x y z)\"];\n\t\tnode3 -> node0 [label=\"'(x y z)\"];\n\t}\n}\n")
+      )
+    (test-case "dynamics%:build-state-graph*"
+      (check-equal? (graphviz (send dyn-syn build-state-graph* (list s1) 2))
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [];\n\t\tnode1 -> node0 [];\n\t}\n}\n")
+      (check-equal? (graphviz (send dyn-syn build-state-graph* (list s1) 'full))
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node3 [];\n\t\tnode1 -> node0 [];\n\t\tnode2 -> node1 [];\n\t\tnode3 -> node2 [];\n\t}\n}\n"))
+    (test-case "dynamics%:build-state-graph/annotated"
+      (check-equal? (graphviz (send dyn-syn build-state-graph/annotated (list s1)))
+                    (graphviz (send dyn-syn build-state-graph*/annotated (list s1) 'full))))
+    (test-case "dynamics%:build-state-graph"
+      (check-equal? (graphviz (send dyn-syn build-state-graph (list s1)))
+                    (graphviz (send dyn-syn build-state-graph* (list s1) 'full))))))
+
+(: make-asyn (-> (Listof Variable) Mode))
+(define (make-asyn vars) (map (inst list Variable) vars))
+
+(module+ test
+  (test-case "make-asyn"
+    (check-equal? (make-asyn '(x y z)) '((x) (y) (z)))))
+
+(: make-syn (-> (Listof Variable) Mode))
+(define (make-syn vars) (list vars))
+
+(module+ test
+  (test-case "make-syn"
+    (check-equal? (make-syn '(x y z)) '((x y z)))))
 
 ;;; Given a network, applies a function for building a mode to its
 ;;; variables and returns the corresponding network dynamics.
-(define (make-dynamics-from-func network mode-func)
-  (dynamics network (mode-func (hash-keys (network-functions network)))))
+(: make-dynamics-from-mode
+   (All (a) (-> (Network a) (-> (Listof Variable) Mode) (Dynamics% a))))
+(define (make-dynamics-from-mode n make-mode)
+  (new (inst dynamics% a)
+       [network n]
+       [mode (make-mode (hash-keys (network-functions n)))]))
 
-;;; Creates the asynchronous dynamics for a given network.
-(define (make-asyn-dynamics network)
-  (make-dynamics-from-func network make-asyn))
-
-;;; Creates the synchronous dynamics for a given network.
-(define (make-syn-dynamics network)
-  (make-dynamics-from-func network make-syn))
+(: make-asyn-dynamics (All (a) (-> (Network a) (Dynamics% a))))
+(define (make-asyn-dynamics [n : (Network a)])
+  ((inst make-dynamics-from-mode a) n make-asyn))
 
 (module+ test
-  (test-case "make-asyn-dynamics, make-syn-dynamics"
-    (define n (forms->boolean-network #hash((a . (not a)) (b . b))))
-    (define asyn (make-asyn-dynamics n))
-    (define syn (make-syn-dynamics n))
-    (check-equal? (dynamics-network asyn) n)
-    (check-equal? (dynamics-mode asyn) (set (set 'a) (set 'b)))
-    (check-equal? (dynamics-network syn) n)
-    (check-equal? (dynamics-mode syn) (set (set 'a 'b)))))
+  (test-case "make-asyn-dynamics"
+    (define n : (Network Boolean)
+      (forms->boolean-network (hash 'x '(not y)
+                                    'y 'x
+                                    'z '(and y z))))
+    (define asyn-dyn (make-asyn-dynamics n))
+    (check-equal? (get-field network asyn-dyn) n)
+    (check-true (set=? (get-field mode asyn-dyn) '((x) (y) (z))))))
 
-;;; Pretty-prints a state of the network.
+(: make-syn-dynamics (All (a) (-> (Network a) (Dynamics% a))))
+(define (make-syn-dynamics [n : (Network a)])
+  ((inst make-dynamics-from-mode a) n make-syn))
+
+(module+ test
+  (test-case "make-syn-dynamics"
+    (define n : (Network Boolean)
+      (forms->boolean-network (hash 'x '(not y)
+                                    'y 'x
+                                    'z '(and y z))))
+    (define syn-dyn (make-syn-dynamics n))
+    (check-equal? (get-field network syn-dyn) n)
+    (define m (get-field mode syn-dyn))
+    (check-equal? (length m) 1)
+    (check-true (set=? (car m) '(x y z)))))
+
+(: pretty-print-state (All (a) (-> (State a) String)))
 (define (pretty-print-state s)
   (string-join (hash-map s (λ (key val) (format "~a:~a" key val)) #t)))
 
@@ -1345,296 +681,325 @@
     (check-equal? (pretty-print-state (hash 'a #f 'b 3 'c 4))
                   "a:#f b:3 c:4")))
 
-;;; Pretty-prints a state of the network to Boolean values 0 or 1.
-(define (pretty-print-boolean-state s)
+(: pretty-print-state/01 (All (a) (-> (State a) String)))
+(define (pretty-print-state/01 s)
   (string-join (hash-map s (λ (key val) (format "~a:~a" key (any->01 val))) #t)))
 
 (module+ test
-  (test-case "pretty-print-boolean-state"
+  (test-case "pretty-print-state/01"
     (check-equal?
-     (pretty-print-boolean-state (hash 'a #f 'b #t 'c #t))
+     (pretty-print-state/01 (hash 'a #f 'b #t 'c #t))
      "a:0 b:1 c:1")))
 
-;;; Given a state graph and a pretty-printer for states build a new
-;;; state graph with pretty-printed vertices and edges.
+(: pretty-print-state-graph-with (-> Graph (-> Any Any) Graph))
 (define (pretty-print-state-graph-with gr pprinter)
-  (update-graph gr #:v-func pprinter #:e-func pretty-print-set-sets))
+  (update-graph
+   gr
+   #:v-func pprinter
+   #:e-func (relax-arg-type/any pretty-print-set-sets (Setof (Setof Any)))))
 
-;;; Pretty prints a state graph with pretty-print-state.
+(: pretty-print-state-graph (-> Graph Graph))
 (define (pretty-print-state-graph gr)
-  (pretty-print-state-graph-with gr pretty-print-state))
+  (define (pprinter/any [x : Any])
+    (pretty-print-state (assert-type x (State Any))))
+  (pretty-print-state-graph-with
+   gr
+   (relax-arg-type/any pretty-print-state (State Any))))
 
-;;; A shortcut for pretty-print-state-graph.
 (define ppsg pretty-print-state-graph)
 
-;;; Pretty prints a state graph with pretty-print-boolean-state.
-(define (pretty-print-boolean-state-graph gr)
-  (pretty-print-state-graph-with gr pretty-print-boolean-state))
+(: pretty-print-state-graph/01 (-> Graph Graph))
+(define (pretty-print-state-graph/01 gr)
+  (define (pprinter/any [x : Any])
+    (pretty-print-state/01 (assert-type x (State Any))))
+  (pretty-print-state-graph-with gr pprinter/any))
 
-;;; A shortcut for pretty-print-boolean-state-graph.
-(define ppsgb pretty-print-boolean-state-graph)
+(define ppsg01 pretty-print-state-graph/01)
 
-;;; Builds the full state graph of a Boolean network.
+(: build-full-state-graph (All (a) (-> (Dynamics% a) Graph)))
 (define (build-full-state-graph dyn)
-  (dds-build-state-graph
-   dyn
-   ((compose list->set
-             build-all-states
-             network-domains
-             dynamics-network) dyn)))
+  (send dyn
+        build-state-graph
+        (build-all-states (network-domains (get-field network dyn)))))
 
-;;; Build the full annotated state graph of a Boolean network.
-(define (build-full-state-graph-annotated dyn)
-  (dds-build-state-graph-annotated
-   dyn
-   ((compose list->set
-             build-all-states
-             network-domains
-             dynamics-network) dyn)))
+(: build-full-state-graph/annotated (All (a) (-> (Dynamics% a) Graph)))
+(define (build-full-state-graph/annotated dyn)
+  (send dyn
+        build-state-graph/annotated
+        (build-all-states (network-domains (get-field network dyn)))))
 
 (module+ test
-  (test-case "Dynamics of networks"
-    (define n (forms->boolean-network #hash((a . (not a)) (b . b))))
-    (define asyn (make-asyn-dynamics n))
-    (define syn (make-syn-dynamics n))
-    (define s (hash 'a #t 'b #f))
-    (define ss (set (hash 'a #t 'b #t)
-                    (hash 'a #f 'b #t)))
-    (define gr1 (dds-build-n-step-state-graph asyn (set s) 1))
-    (define gr-full (dds-build-state-graph asyn (set s)))
-    (define gr-full-pp (pretty-print-state-graph gr-full))
-    (define gr-full-ppb (pretty-print-boolean-state-graph gr-full))
-    (define gr-complete-bool (build-full-state-graph asyn))
-    (define gr-complete-bool-ann (build-full-state-graph-annotated asyn))
-    (check-equal? (dds-step-one asyn s) (set (hash 'a #f 'b #f)
-                                             (hash '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 (hash 'a #f 'b #f)))
-    (check-equal? (dds-step asyn ss)
-                  (set (hash 'a #f 'b #t)
-                       (hash 'a #t 'b #t)))
-    (check-true (has-vertex? gr1 #hash((a . #t) (b . #f))))
-    (check-true (has-vertex? gr1 #hash((a . #f) (b . #f))))
-    (check-false (has-vertex? gr1 #hash((a . #t) (b . #t))))
-    (check-true (has-edge? gr1 #hash((a . #t) (b . #f)) #hash((a . #f) (b . #f))))
-    (check-true (has-edge? gr1 #hash((a . #t) (b . #f)) #hash((a . #t) (b . #f))))
-    (check-false (has-edge? gr1 #hash((a . #f) (b . #f)) #hash((a . #t) (b . #f))))
+  (let* ([n1 : (Network Boolean)
+             (forms->boolean-network (hash 'x '(not y)
+                                           'y 'x
+                                           'z '(and y z)))]
+         [dyn-syn (make-syn-dynamics n1)]
+         [sg ((inst build-full-state-graph Boolean) dyn-syn)]
+         [sg/an ((inst build-full-state-graph/annotated Boolean) dyn-syn)])
+    (test-case "build-full-state-graph"
+      (check-equal? (graphviz sg)
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode7 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [];\n\t\tnode1 -> node7 [];\n\t\tnode2 -> node4 [];\n\t\tnode3 -> node7 [];\n\t\tnode4 -> node1 [];\n\t\tnode5 -> node1 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node6 [];\n\t}\n}\n"))
+    (test-case "build-full-state-graph/annotated"
+      (check-equal? (graphviz sg/an)
+                    "digraph G {\n\tnode0 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode4 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode7 [label=\"'#hash((x . #f) (y . #f) (z . #f))\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node2 [label=\"'(z y x)\"];\n\t\tnode1 -> node6 [label=\"'(z y x)\"];\n\t\tnode2 -> node4 [label=\"'(z y x)\"];\n\t\tnode3 -> node6 [label=\"'(z y x)\"];\n\t\tnode4 -> node1 [label=\"'(z y x)\"];\n\t\tnode5 -> node7 [label=\"'(z y x)\"];\n\t\tnode6 -> node5 [label=\"'(z y x)\"];\n\t\tnode7 -> node1 [label=\"'(z y x)\"];\n\t}\n}\n"))
 
-    (check-true (has-vertex? gr-full #hash((a . #t) (b . #f))))
-    (check-true (has-vertex? gr-full #hash((a . #f) (b . #f))))
-    (check-false (has-vertex? gr-full #hash((a . #t) (b . #t))))
-    (check-true (has-edge? gr-full #hash((a . #t) (b . #f)) #hash((a . #f) (b . #f))))
-    (check-true (has-edge? gr-full #hash((a . #t) (b . #f)) #hash((a . #t) (b . #f))))
-    (check-true (has-edge? gr-full #hash((a . #f) (b . #f)) #hash((a . #t) (b . #f))))
-    (check-true (has-edge? gr-full #hash((a . #f) (b . #f)) #hash((a . #f) (b . #f))))
+    (test-case "pretty-print-state-graph, pretty-print-state-graph/boolean"
+      (check-equal? (graphviz (ppsg sg))
+                    "digraph G {\n\tnode0 [label=\"x:#f y:#t z:#f\"];\n\tnode1 [label=\"x:#f y:#t z:#t\"];\n\tnode2 [label=\"x:#t y:#f z:#t\"];\n\tnode3 [label=\"x:#t y:#t z:#t\"];\n\tnode4 [label=\"x:#t y:#t z:#f\"];\n\tnode5 [label=\"x:#t y:#f z:#f\"];\n\tnode6 [label=\"x:#f y:#f z:#f\"];\n\tnode7 [label=\"x:#f y:#f z:#t\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node6 [];\n\t\tnode1 -> node7 [];\n\t\tnode2 -> node4 [];\n\t\tnode3 -> node1 [];\n\t\tnode4 -> node0 [];\n\t\tnode5 -> node4 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node5 [];\n\t}\n}\n")
+      (check-equal? (graphviz (ppsg01 sg))
+                    "digraph G {\n\tnode0 [label=\"x:1 y:0 z:0\"];\n\tnode1 [label=\"x:0 y:1 z:1\"];\n\tnode2 [label=\"x:0 y:0 z:1\"];\n\tnode3 [label=\"x:1 y:1 z:1\"];\n\tnode4 [label=\"x:1 y:0 z:1\"];\n\tnode5 [label=\"x:0 y:1 z:0\"];\n\tnode6 [label=\"x:0 y:0 z:0\"];\n\tnode7 [label=\"x:1 y:1 z:0\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node7 [];\n\t\tnode1 -> node2 [];\n\t\tnode2 -> node0 [];\n\t\tnode3 -> node1 [];\n\t\tnode4 -> node7 [];\n\t\tnode5 -> node6 [];\n\t\tnode6 -> node0 [];\n\t\tnode7 -> node5 [];\n\t}\n}\n"))))
 
-    (check-true (has-vertex? gr-full-pp "a:#f b:#f"))
-    (check-true (has-vertex? gr-full-pp "a:#t b:#f"))
-    (check-true (has-vertex? gr-full-ppb "a:0 b:0"))
-    (check-true (has-vertex? gr-full-ppb "a:1 b:0"))
-
-    (check-true (set=?
-                 (get-edges gr-complete-bool)
-                 '((#hash((a . #f) (b . #f)) #hash((a . #t) (b . #f)))
-                   (#hash((a . #f) (b . #f)) #hash((a . #f) (b . #f)))
-                   (#hash((a . #t) (b . #f)) #hash((a . #t) (b . #f)))
-                   (#hash((a . #t) (b . #f)) #hash((a . #f) (b . #f)))
-                   (#hash((a . #t) (b . #t)) #hash((a . #f) (b . #t)))
-                   (#hash((a . #t) (b . #t)) #hash((a . #t) (b . #t)))
-                   (#hash((a . #f) (b . #t)) #hash((a . #f) (b . #t)))
-                   (#hash((a . #f) (b . #t)) #hash((a . #t) (b . #t))))))
-
-    (check-true (set=?
-                 (get-edges gr-complete-bool-ann)
-                 '((#hash((a . #f) (b . #f)) #hash((a . #t) (b . #f)))
-                   (#hash((a . #f) (b . #f)) #hash((a . #f) (b . #f)))
-                   (#hash((a . #t) (b . #f)) #hash((a . #t) (b . #f)))
-                   (#hash((a . #t) (b . #f)) #hash((a . #f) (b . #f)))
-                   (#hash((a . #t) (b . #t)) #hash((a . #f) (b . #t)))
-                   (#hash((a . #t) (b . #t)) #hash((a . #t) (b . #t)))
-                   (#hash((a . #f) (b . #t)) #hash((a . #f) (b . #t)))
-                   (#hash((a . #f) (b . #t)) #hash((a . #t) (b . #t))))))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #f) (b . #f)) #hash((a . #t) (b . #f)))
-                  (set (set 'a)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #f) (b . #f)) #hash((a . #f) (b . #f)))
-                  (set (set 'b)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #t) (b . #f)) #hash((a . #t) (b . #f)))
-                  (set (set 'b)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #t) (b . #f)) #hash((a . #f) (b . #f)))
-                  (set (set 'a)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #t) (b . #t)) #hash((a . #f) (b . #t)))
-                  (set (set 'a)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #t) (b . #t)) #hash((a . #t) (b . #t)))
-                  (set (set 'b)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #f) (b . #t)) #hash((a . #f) (b . #t)))
-                  (set (set 'b)))
-    (check-equal? (edge-weight gr-complete-bool-ann
-                               #hash((a . #f) (b . #t)) #hash((a . #t) (b . #t)))
-                  (set (set 'a)))))
-
-
-;;; =================================
-;;; Tabulating functions and networks
-;;; =================================
-
-
-;;; Like tabulate, but supposes that the function works on states.
-;;;
-;;; The argument domains defines the domains of each of the component
-;;; of the states.  If headers it true, the resulting list starts with
-;;; a listing the names of the variables of the domain and ending with
-;;; the symbol 'f, which indicates the values of the function.
-(define (tabulate-state func domains #:headers [headers #t])
-  (define tab (tabulate-state* `(,func) domains #:headers headers))
-  (cond
-    [headers
-     ;; Replace 'f1 in the headers by 'f.
-     (match tab [(cons hdrs vals)
-                 (cons (append (drop-right hdrs 1) '(f)) vals)])]
-    [else tab]))
-
-;;; Like tabulate-state, but assumes the function is a Boolean
-;;; function.  args is a list of names of the arguments which can
-;;; appear in the states.
-(define (tabulate-state/boolean func args #:headers [headers #t])
-  (tabulate-state func (make-boolean-domains args) #:headers headers))
+(: tabulate-state* (All (a) (-> (Listof (-> (State a) a)) (DomainMapping a)
+                                (Listof (Listof a)))))
+(define (tabulate-state* funcs domains)
+  (for/list : (Listof (Listof a)) ([s (in-list (build-all-states domains))])
+    (append (hash-map s (λ ([x : Variable] [y : a]) y) #t)
+            (for/list : (Listof a) ([f (in-list funcs)]) (f s)))))
 
 (module+ test
-  (test-case "tabulate-state/boolean"
-    (define func (λ (st) (not (hash-ref st 'a))))
-    (check-equal? (tabulate-state/boolean func '(a)) '((a f) (#f #t) (#t #f)))))
+  (test-case "tabulate-state*"
+    (define/: f1 (State Integer) (+ :a :b))
+    (define/: f2 (State Integer) (- :a :b))
+    (check-equal? (tabulate-state* (list f1 f2) (hash 'a '(1 2) 'b '(2 3)))
+                  '((1 2 3 -1)
+                    (1 3 4 -2)
+                    (2 2 4  0)
+                    (2 3 5 -1)))))
 
-;;; Like tabulate-state, but takes a list of functions over the same
-;;; domain.  If headers is #t, the first list of the result enumerates
-;;; the variable names, and then contains a symbol 'fi for each of the
-;;; functions, where i is replaced by the number of the function in
-;;; the list.
-(define (tabulate-state* funcs domains #:headers [headers #t])
-  (define tab (for/list ([st (build-all-states domains)])
-                (append (hash-map st (λ (x y) y) #t)
-                        (for/list ([f funcs]) (f st)))))
-  (cond
-    [headers
-     (define var-names (hash-map domains (λ (x y) x) #t))
-     (define func-names (for/list ([_ funcs] [i (in-naturals 1)]) (string->symbol (format "f~a" i))))
-     (cons (append var-names func-names) tab)]
-    [else tab]))
+(: tabulate-state*+headers
+   (All (a) (-> (Listof (-> (State a) a)) (DomainMapping a)
+                (Pairof (Listof Symbol) (Listof (Listof a))))))
+(define (tabulate-state*+headers funcs domains)
+  (define var-names : (Listof Symbol)
+    (hash-map domains (λ ([x : Symbol] _) x) #t))
+  (define func-names : (Listof Symbol)
+    (for/list ([_ funcs]
+               [i (in-naturals 1)])
+      (string->symbol (~a 'f i))))
+  (cons (append var-names func-names)
+        (tabulate-state* funcs domains)))
 
-;;; Like tabulate-state/boolean, but takes a list of functions.
-(define (tabulate-state*/boolean funcs args #:headers [headers #t])
-  (tabulate-state* funcs (make-boolean-domains args) #:headers headers))
+(module+ test
+  (test-case "tabulate-state*+headers"
+    (define/: f1 (State Integer) (+ :a :b))
+    (define/: f2 (State Integer) (- :a :b))
+    (check-equal?
+     (tabulate-state*+headers (list f1 f2) (hash 'a '(1 2) 'b '(2 3)))
+     '((a b f1 f2)
+       (1 2 3 -1)
+       (1 3 4 -2)
+       (2 2 4 0)
+       (2 3 5 -1)))))
+
+(: tabulate-state*/boolean
+   (-> (Listof (-> (State Boolean) Boolean)) (Listof Variable)
+       (Listof (Listof Boolean))))
+(define (tabulate-state*/boolean funcs args)
+  (tabulate-state* funcs (make-boolean-domains args)))
 
 (module+ test
   (test-case "tabulate-state*/boolean"
-    (define f1 (λ (st) (and (hash-ref st 'a) (hash-ref st 'b))))
-    (define f2 (λ (st) (or (hash-ref st 'a) (hash-ref st 'b))))
+    (define/: f1 (State Boolean) (and :a :b))
+    (define/: f2 (State Boolean) (or :a :b))
     (check-equal? (tabulate-state*/boolean (list f1 f2) '(a b))
+                  '((#f #f #f #f)
+                    (#f #t #f #t)
+                    (#t #f #f #t)
+                    (#t #t #t #t)))))
+
+(: tabulate-state*+headers/boolean
+   (-> (Listof (-> (State Boolean) Boolean)) (Listof Variable)
+       (Pairof (Listof Symbol) (Listof (Listof Boolean)))))
+(define (tabulate-state*+headers/boolean funcs args)
+  (tabulate-state*+headers funcs (make-boolean-domains args)))
+
+(module+ test
+  (test-case "tabulate-state*+headers/boolean"
+    (define/: f1 (State Boolean) (and :a :b))
+    (define/: f2 (State Boolean) (or :a :b))
+    (check-equal? (tabulate-state*+headers/boolean (list f1 f2) '(a b))
                   '((a b f1 f2)
                     (#f #f #f #f)
                     (#f #t #f #t)
                     (#t #f #f #t)
                     (#t #t #t #t)))))
 
-;;; Tabulates a given network.
-;;;
-;;; For a Boolean network with n variables, returns a table with 2n
-;;; columns and 2^n rows.  The first n columns correspond to the
-;;; different values of the variables of the networks.  The last n
-;;; columns represent the values of the n update functions of the
-;;; network.  If headers is #t, prepends a list of variable names and
-;;; update functions (f-x, where x is the name of the corresponding
-;;; variable) to the result.
-(define (tabulate-network network #:headers [headers #t])
-  ;; I use hash-map with try-order? set to #t to ask the hash table to
-  ;; sort the keys for me.
-  (define-values (vars funcs) (for/lists (l1 l2)
-                                         ([pair (hash-map (network-functions network) cons #t)])
-                                (values (car pair) (cdr pair))))
-  (define tab (tabulate-state* funcs (network-domains network) #:headers headers))
-  (cond
-    [headers
-     ;; Replace the names of the functions tabulate-state* gave us by
-     ;; what we promise in the comment.
-     (define fnames (for/list ([x (in-list vars)])
-                      (string->symbol (format "f-~a" x))))
-     (match tab [(cons hdrs vals)
-                 (cons (append (take hdrs (length vars)) fnames) vals)])]
-    [else tab]))
+(define-syntax-parse-rule (make-tabulate-no-star name star-name)
+  (define (name func domains)
+    (star-name `(,func) domains)))
+
+(: tabulate-state (All (a) (-> (-> (State a) a) (DomainMapping a)
+                               (Listof (Listof a)))))
+(make-tabulate-no-star tabulate-state tabulate-state*)
+
+(module+ test
+  (test-case "tabulate-state"
+    (check-equal? (tabulate-state (λ/: (State Integer) (+ :a :b))
+                                  (hash 'a '(1 2) 'b '(2 3)))
+                  '((1 2 3)
+                    (1 3 4)
+                    (2 2 4)
+                    (2 3 5)))))
+
+(: tabulate-state+headers (All (a) (-> (-> (State a) a) (DomainMapping a)
+                                       (Pairof (Listof Symbol)
+                                               (Listof (Listof a))))))
+(make-tabulate-no-star tabulate-state+headers tabulate-state*+headers)
+
+(module+ test
+  (test-case "tabulate-state+headers"
+    (check-equal? (tabulate-state+headers
+                   (λ/: (State Integer) (+ :a :b))
+                   (hash 'a '(1 2) 'b '(2 3)))
+                  '((a b f1)
+                    (1 2 3)
+                    (1 3 4)
+                    (2 2 4)
+                    (2 3 5)))))
+
+(: tabulate-state/boolean
+   (-> (-> (State Boolean) Boolean)
+       (Listof Variable)
+       (Listof (Listof Boolean))))
+(make-tabulate-no-star tabulate-state/boolean tabulate-state*/boolean)
+
+(module+ test
+  (test-case "tabulate-state/boolean"
+    (check-equal? (tabulate-state/boolean (λ/: (State Boolean) (and :a :b)) '(a b))
+                  '((#f #f #f)
+                    (#f #t #f)
+                    (#t #f #f)
+                    (#t #t #t)))))
+
+(: tabulate-state+headers/boolean
+   (-> (-> (State Boolean) Boolean)
+       (Listof Variable)
+       (Pairof (Listof Symbol) (Listof (Listof Boolean)))))
+(make-tabulate-no-star tabulate-state+headers/boolean tabulate-state*+headers/boolean)
+
+(module+ test
+  (test-case "tabulate-state+headers/boolean"
+    (check-equal? (tabulate-state+headers/boolean
+                   (λ/: (State Boolean) (and :a :b)) '(a b))
+                  '((a b f1)
+                    (#f #f #f)
+                    (#f #t #f)
+                    (#t #f #f)
+                    (#t #t #t)))))
+
+(: tabulate-network (All (a) (-> (Network a) (Listof (Listof a)))))
+(define (tabulate-network network)
+  (define funcs (hash-map (network-functions network)
+                          (λ (_ [fx : (UpdateFunction a)]) fx)
+                          #t))
+  (tabulate-state* funcs (network-domains network)))
 
 (module+ test
   (test-case "tabulate-network"
-    (define bn (forms->boolean-network #hash((a . (not a)) (b . b))))
+    (define bn (forms->boolean-network (hash 'a '(not a) 'b 'b)))
     (check-equal? (tabulate-network bn)
-                  '((a b f-a f-b) (#f #f #t #f) (#f #t #t #t) (#t #f #f #f) (#t #t #f #t)))
-    (check-equal? (tabulate-network bn #:headers #f)
-                  '((#f #f #t #f) (#f #t #t #t) (#t #f #f #f) (#t #t #f #t)))))
+                  '((#f #f #t #f)
+                    (#f #t #t #t)
+                    (#t #f #f #f)
+                    (#t #t #f #t)))))
 
+(: tabulate-network+headers (All (a) (-> (Network a)
+                                         (Pairof (Listof Symbol)
+                                                 (Listof (Listof a))))))
+(define (tabulate-network+headers network)
+  (define-values (vars funcs)
+    (for/lists ([l1 : (Listof Variable)]
+                [l2 : (Listof (UpdateFunction a))])
+               ([p (hash-map (network-functions network)
+                             (inst cons Variable (UpdateFunction a))
+                             #t)])
+      (values (car p) (cdr p))))
 
-;;; ===================================
-;;; Constructing functions and networks
-;;; ===================================
+  (define fnames : (Listof Variable)
+    (for/list ([v vars]) (format-symbol "f-~a" v)))
 
-;;; Given a table like the one produced by tabulate-network,
-;;; constructs a Boolean network having this behaviour.  If headers is
-;;; #t, considers that the first element of the list are the headers
-;;; and reads the names of the variables from them.  Otherwise
-;;; generates names for variables of the form xi, where 0 ≤ i < number
-;;; of variables, and treats all rows in the table as defining the
-;;; behaviour of the functions of the network.  The columns defining
-;;; the functions are taken to be in the same order as the variables
-;;; in the first half of the function.  The headers of the columns
-;;; defining the functions are therefore discarded.
-;;;
-;;; This function relies on table->function, so the same caveats
-;;; apply.
-;;;
-;;; The domains of the network is a mapping assigning to each variable
-;;; the set of values which can appear in its column in the table.
-;;; This function does not check whether the table is complete.
-(define (table->network table #:headers [headers #t])
-  (define n (/ (length (car table)) 2))
-  ;; Get the variable names from the table or generate them, if
-  ;; necessary.
-  (define var-names (cond [headers (take (car table) n)]
-                          [else (for ([i (in-range n)])
-                                  (symbol->string (format "x~a" i)))]))
-  ;; Drop the headers if they are present.
-  (define tab (cond [headers (cdr table)]
-                    [else table]))
+  (match (tabulate-state*+headers funcs (network-domains network))
+    [(list headers tab ...)
+     (cons (append (take headers (length fnames)) fnames)
+           tab)]))
+
+(module+ test
+  (test-case "tabulate-network+headers"
+    (define bn (forms->boolean-network (hash 'a '(not a) 'b 'b)))
+    (check-equal? (tabulate-network+headers bn)
+                  '((a b f-a f-b)
+                    (#f #f #t #f)
+                    (#f #t #t #t)
+                    (#t #f #f #f)
+                    (#t #t #f #t)))))
+
+(: table+vars->network (All (a) (-> (Listof Variable) (Listof (Listof a))
+                                    (Network a))))
+(define (table+vars->network var-names table)
+  (define n : Integer (quotient (length (car table)) 2))
   ;; Split the table into the inputs and the outputs of the functions.
-  (define-values (ins outs) (multi-split-at tab n))
+  (define-values (ins outs) (multi-split-at table n))
   ;; Transpose outs to have functions define by lines instead of by
   ;; columns.
-  (define func-lines (lists-transpose outs))
+  (define func-lines : (Listof (Listof a)) (lists-transpose outs))
   ;; Make states out of inputs.
-  (define st-ins (for/list ([in ins]) (make-immutable-hash (map cons var-names in))))
+  (define st-ins : (Listof (State a))
+    (for/list ([in ins]) (make-immutable-hash
+                          (map (inst cons Variable a) var-names in))))
   ;; Construct the functions.
-  (define funcs (for/list ([out func-lines])
-                  (table->function (for/list ([in st-ins] [o out])
-                                     (list in o)))))
+  (define funcs : (Listof (UpdateFunction a))
+    (for/list ([out func-lines])
+      (table->unary-function
+       (for/list : (Listof (List (State a) a))
+                 ([in st-ins] [o out])
+         (list in o)))))
   ;; Infer the domains.
-  (define domains (for/hash [(dom (in-list (lists-transpose ins)))
-                             (x (in-list var-names))]
-                    (values x (remove-duplicates dom))))
+  (define domains : (DomainMapping a)
+    (make-immutable-hash
+     (map (inst cons Variable (Domain a))
+          var-names
+          (map (inst remove-duplicates a) (lists-transpose ins)))))
   ;; Construct the network.
-  (network (for/hash ([x (in-list var-names)]
-                      [f (in-list funcs)])
-             (values x f))
+  (network (make-immutable-hash
+            (map (inst cons Variable (UpdateFunction a))
+                 var-names funcs))
            domains))
 
+(module+ test
+  (test-case "table+vars->network"
+    (define n (table+vars->network '(x1 x2)
+                                   '((#f #f #f #f)
+                                     (#f #t #f #t)
+                                     (#t #f #t #f)
+                                     (#t #t #t #t))))
+    (define f1 (hash-ref (network-functions n) 'x1))
+    (define f2 (hash-ref (network-functions n) 'x2))
+
+    (check-false (f1 (hash 'x1 #f 'x2 #f)))
+    (check-false (f1 (hash 'x1 #f 'x2 #t)))
+    (check-true (f1 (hash 'x1 #t 'x2 #f)))
+    (check-true (f1 (hash 'x1 #t 'x2 #t)))
+
+    (check-false (f2 (hash 'x1 #f 'x2 #f)))
+    (check-true (f2 (hash 'x1 #f 'x2 #t)))
+    (check-false (f2 (hash 'x1 #t 'x2 #f)))
+    (check-true (f2 (hash 'x1 #t 'x2 #t)))
+
+    (check-equal? (network-domains n)
+                  #hash((x1 . (#f #t)) (x2 . (#f #t))))))
+
+(: table->network (All (a) (-> (Listof (Listof a)) (Network a))))
+(define (table->network table)
+  (define n : Integer (quotient (length (car table)) 2))
+  (define var-names : (Listof Variable)
+    (for/list : (Listof Variable)
+              ([i (in-range 1 (add1 n))])
+      (format-symbol "x~a" i)))
+  (table+vars->network var-names table))
+
 (module+ test
   (test-case "table->network"
-    (define n (table->network '((x1 x2 f1 f2)
-                                (#f #f #f #f)
+    (define n (table->network '((#f #f #f #f)
                                 (#f #t #f #t)
                                 (#t #f #t #f)
                                 (#t #t #t #t))))
@@ -1654,772 +1019,112 @@
     (check-equal? (network-domains n)
                   #hash((x1 . (#f #t)) (x2 . (#f #t))))))
 
+(: table+headers->network (All (a) (-> (Pairof (Listof Symbol) (Listof (Listof a)))
+                                       (Network a))))
+(define (table+headers->network table)
+  (define headers : (Listof Symbol) (car table))
+  (define var-names : (Listof Variable)
+    (drop-right headers (quotient (length headers) 2)))
+  (table+vars->network var-names (cdr table)))
 
-;;; =============================
-;;; Random functions and networks
-;;; =============================
+(module+ test
+  (test-case "table+headers->network"
+    (define n (table+headers->network
+               '((x1 x2 f1 f2)
+                 (#f #f #f #f)
+                 (#f #t #f #t)
+                 (#t #f #t #f)
+                 (#t #t #t #t))))
+    (define f1 (hash-ref (network-functions n) 'x1))
+    (define f2 (hash-ref (network-functions n) 'x2))
 
-;;; Generates a random function accepting a state over the domains
-;;; given by arg-domains and producing values in func-domain.
+    (check-false (f1 (hash 'x1 #f 'x2 #f)))
+    (check-false (f1 (hash 'x1 #f 'x2 #t)))
+    (check-true (f1 (hash 'x1 #t 'x2 #f)))
+    (check-true (f1 (hash 'x1 #t 'x2 #t)))
+
+    (check-false (f2 (hash 'x1 #f 'x2 #f)))
+    (check-true (f2 (hash 'x1 #f 'x2 #t)))
+    (check-false (f2 (hash 'x1 #t 'x2 #f)))
+    (check-true (f2 (hash 'x1 #t 'x2 #t)))
+
+    (check-equal? (network-domains n)
+                  #hash((x1 . (#f #t)) (x2 . (#f #t))))))
+
+(: random-function/state (All (a) (-> (DomainMapping a) (Domain a)
+                                      (-> (State a) a))))
 (define (random-function/state arg-domains func-domain)
-  (table->function (for/list ([st (build-all-states arg-domains)])
-                     (list st (random-ref func-domain)))))
+  (table->unary-function
+   (for/list : (Listof (List (State a) a))
+             ([st (build-all-states arg-domains)])
+     (list st (random-ref func-domain)))))
 
-;;; Like random-function/state, but the domains of the arguments and
-;;; of the function are Boolean.  args is a list of names of the
-;;; variables appearing in the state.
+(module+ test (random-seed 1))
+
+(module+ test
+  (test-case "random-function/state"
+    (define doms (hash 'a '(1 2) 'b '(3 4)))
+    (define f (random-function/state doms '(e f)))
+    (check-equal? (tabulate-state+headers f doms)
+                  '((a b f1) (1 3 e) (1 4 e) (2 3 f) (2 4 e)))))
+
+(: random-boolean-function/state (-> (Listof Variable) (-> (State Boolean) Boolean)))
 (define (random-boolean-function/state args)
   (random-function/state (make-boolean-domains args) '(#f #t)))
 
 (module+ test
   (test-case "random-boolean-function/state"
-    (random-seed 0)
     (define f (random-boolean-function/state '(x1 x2)))
-    (check-equal? (tabulate-state/boolean f '(x1 x2))
-                  '((x1 x2 f) (#f #f #f) (#f #t #f) (#t #f #t) (#t #t #t)))
-    (check-equal? (tabulate-state/boolean f '(x1 x2) #:headers #f)
-                  '((#f #f #f) (#f #t #f) (#t #f #t) (#t #t #t)))
-    (define bn (random-boolean-network/vars 3))
-    (check-equal? (tabulate-network bn)
-                  '((x0 x1 x2 f-x0 f-x1 f-x2)
-                    (#f #f #f #f #t #f)
-                    (#f #f #t #t #f #f)
-                    (#f #t #f #f #t #t)
-                    (#f #t #t #t #f #f)
-                    (#t #f #f #t #f #t)
-                    (#t #f #t #f #f #t)
-                    (#t #t #f #f #f #f)
-                    (#t #t #t #t #t #t)))))
+    (check-equal? (tabulate-state+headers/boolean f '(x1 x2))
+                  '((x1 x2 f1) (#f #f #f) (#f #t #f) (#t #f #t) (#t #t #t)))))
 
-;;; Generates a random network from the given domain mapping.
+(: random-network (All (a) (-> (DomainMapping a) (Network a))))
 (define (random-network domains)
-  (network (for/hash ([(x x-dom) (in-hash domains)])
+  (network (for/hash : (VariableMapping (UpdateFunction a))
+                     ([(x x-dom) (in-hash domains)])
              (values x (random-function/state domains x-dom)))
            domains))
 
-;;; Generates a random Boolean network with the given variables.
+(module+ test
+  (test-case "random-network"
+    (check-equal?
+     (tabulate-network+headers (random-network (hash 'a '(1 2) 'b '(#f #t))))
+     '((a b f-a f-b) (1 #f 1 #f) (1 #t 1 #f) (2 #f 2 #t) (2 #t 2 #f)))))
+
+(: random-boolean-network (-> (Listof Variable) (Network Boolean)))
 (define (random-boolean-network vars)
   (random-network (make-boolean-domains vars)))
 
-;;; Like random-boolean-network, but also generates the names of the
-;;; variables for the network.  The variables have the names x0 to xk,
-;;; where k = n - 1.
-(define (random-boolean-network/vars n)
-  (random-boolean-network (for/list ([i (in-range n)]) (string->symbol (format "x~a" i)))))
-
-
-;;; ===================
-;;; TBF/TBN and SBF/SBN
-;;; ===================
-
-;;; Applies a TBF to a state.
-;;;
-;;; The values of the variables of the state are ordered by hash-map
-;;; and fed to the TBF in order.  The number of the inputs of the TBF
-;;; must match the number of variables in the state.
-(define (apply-tbf-to-state tbf st)
-  (apply-tbf tbf (list->vector (hash-map st (λ (_ val) val)))))
-
 (module+ test
-  (test-case "apply-tbf-to-state"
-    (define st (hash 'x1 0 'x2 1))
-    (define f (tbf #(1 1) 1))
-    (check-equal? (apply-tbf-to-state f st) 0)))
-
-;;; A state TBF is a TBF with named inputs.  A state TBF can be
-;;; applied to states in an unambiguous ways.
-(struct tbf/state (weights threshold) #:transparent)
-
-;;; Shortcuts for acessing fields of a state/tbf.
-(define tbf/state-w tbf/state-weights)
-(define tbf/state-θ tbf/state-threshold)
-
-;;; Makes a state/tbf from a list of pairs of names of variables and
-;;; weights, as well as a threshold.
-(define (make-tbf/state pairs threshold)
-  (tbf/state (make-immutable-hash pairs) threshold))
-
-(module+ test
-  (test-case "tbf/state"
-    (define f (make-tbf/state '((x1 . 1) (x2 . 1)) 1))
-    (check-equal? (tbf/state-w f) #hash((x1 . 1) (x2 . 1)))
-    (check-equal? (tbf/state-θ f) 1)))
-
-;;; A sign Boolean function (SBF) is a TBF whose threshold is 0.
-(define sbf/state? (and/c tbf/state? (λ (tbf) (zero? (tbf/state-θ tbf)))))
-
-(module+ test
-  (test-case "sbf/state?"
-    (check-true (sbf/state? (tbf/state #hash((a . -1) (b . 1)) 0)))))
-
-;;; Makes a state/tbf which is an SBF from a list of pairs of names of
-;;; variables and weights.
-(define (make-sbf/state pairs)
-  (make-tbf/state pairs 0))
-
-(module+ test
-  (test-case "make-sbf/state"
-    (check-equal? (make-sbf/state '((a . -1) (b . 1)))
-                  (make-tbf/state '((a . -1) (b . 1)) 0))))
-
-;;; Applies a state TBF to its inputs.
-;;;
-;;; Applying a TBF consists in multiplying the weights by the
-;;; corresponding inputs and comparing the sum of the products to the
-;;; threshold.
-;;;
-;;; This function is similar to apply-tbf, but applies a state TBF (a
-;;; TBF with explicitly named inputs) to a state whose values are 0
-;;; and 1.
-(define (apply-tbf/state tbf st)
-  (any->01 (> (foldl + 0 (hash-values
-                          (hash-intersect (tbf/state-w tbf)
-                                          st
-                                          #:combine *)))
-              (tbf/state-θ tbf))))
-
-(module+ test
-  (test-case "apply-tbf/state"
-    (define st1 (hash 'a 1 'b 0 'c 1))
-    (define st2 (hash 'a 1 'b 1 'c 0))
-    (define tbf (make-tbf/state '((a . 2) (b . -2)) 1))
-    (check-equal? (apply-tbf/state tbf st1) 1)
-    (check-equal? (apply-tbf/state tbf st2) 0)))
-
-;;; Reads a list of tbf/state from a list of list of numbers.
-;;;
-;;; The last element of each list is taken to be the threshold of the
-;;; TBFs, and the rest of the elements are taken to be the weights.
-;;;
-;;; If headers is #t, the names of the variables to appear as the
-;;; inputs of the TBF are taken from the first list.  The last element
-;;; of this list is discarded.
-;;;
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-(define (lists->tbfs/state lsts #:headers [headers #t])
-  (define-values (var-names rows)
-    (if headers
-        (values (car lsts) (cdr lsts))
-        (values (for/list ([i (in-range (length (car lsts)))])
-                  (string->symbol (format "x~a" i)))
-                lsts)))
-  (for/list ([lst (in-list rows)])
-    (define-values (ws θ) (split-at-right lst 1))
-    (make-tbf/state (for/list ([x (in-list var-names)]
-                               [w (in-list ws)])
-                      (cons x w))
-                    (car θ))))
-
-(module+ test
-  (test-case "lists->tbfs/state"
-    (define tbfs '((1 2 3) (1 1 2)))
-    (check-equal? (lists->tbfs/state tbfs #:headers #f)
-                  (list
-                   (tbf/state '#hash((x0 . 1) (x1 . 2)) 3)
-                   (tbf/state '#hash((x0 . 1) (x1 . 1)) 2)))
-    (check-equal? (lists->tbfs/state (cons '(a b f) tbfs))
-                  (list
-                   (tbf/state '#hash((a . 1) (b . 2)) 3)
-                   (tbf/state '#hash((a . 1) (b . 1)) 2)))))
-
-;;; Like lists->tbfs/state, but does not expect thresholds in the
-;;; input.
-;;;
-;;; Every lists in the list contains the weights of the SBF.  If
-;;; headers is #t, the names of the variables to appear as the inputs
-;;; of the TBF are taken from the first list.
-;;;
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-(define (lists->sbfs/state lsts #:headers [headers #t])
-  (define rows (if headers (cdr lsts) lsts))
-  (define rows-θ (for/list ([lst (in-list rows)]) (append lst '(0))))
-  (lists->tbfs/state (if headers (cons (car lsts) rows-θ) rows-θ)
-                     #:headers headers))
-
-(module+ test
-  (test-case "lists->sbfs/state"
-    (define tbfs '((1 2) (1 -1)))
-    (check-equal? (lists->sbfs/state tbfs #:headers #f)
-                  (list
-                   (tbf/state '#hash((x0 . 1) (x1 . 2)) 0)
-                   (tbf/state '#hash((x0 . 1) (x1 . -1)) 0)))
-    (check-equal? (lists->sbfs/state (cons '(a b) tbfs) #:headers #t)
-                  (list
-                   (tbf/state '#hash((a . 1) (b . 2)) 0)
-                   (tbf/state '#hash((a . 1) (b . -1)) 0)))))
-
-;;; Reads a list of tbf/state from an Org-mode string containing a
-;;; sexp, containing a list of lists of numbers.  As in
-;;; lists->tbfs/state, the last element of each list is taken to be
-;;; the threshold of the TBFs, and the rest of the elements are taken
-;;; to be the weights.
-;;;
-;;; If headers is #t, the names of the variables to appear as the
-;;; inputs of the TBF are taken from the first list.  The last element
-;;; of this list is discarded.
-;;;
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-(define (read-org-tbfs/state str #:headers [headers #t])
-  (lists->tbfs/state (read-org-sexp str) #:headers headers))
-
-(module+ test
-  (test-case "read-org-tbfs/state"
-    (check-equal? (read-org-tbfs/state "((a b f) (1 2 3) (1 1 2))")
-                  (list
-                   (tbf/state '#hash((a . 1) (b . 2)) 3)
-                   (tbf/state '#hash((a . 1) (b . 1)) 2)))
-    (check-equal? (read-org-tbfs/state "((1 2 3) (1 1 2))" #:headers #f)
-                  (list
-                   (tbf/state '#hash((x0 . 1) (x1 . 2)) 3)
-                   (tbf/state '#hash((x0 . 1) (x1 . 1)) 2)))))
-
-;;; Like read-org-tbfs/state, but reads a list of SBFs.  Therefore,
-;;; the lists of numbers in the sexp are taken to be the weights of
-;;; the SBFs.
-;;;
-;;; If headers is #t, the names of the variables to appear as the
-;;; inputs of the TBF are taken from the first list.  If headers is
-;;; #f, the names of the variables are generated as xi, where i is the
-;;; index of the variable.
-(define (read-org-sbfs/state str #:headers [headers #t])
-  (lists->sbfs/state (read-org-sexp str) #:headers headers))
-
-(module+ test
-  (test-case "read-org-sbfs/state"
-    (check-equal? (read-org-sbfs/state "((a b) (-1 2) (1 1))")
-                  (list
-                   (tbf/state '#hash((a . -1) (b . 2)) 0)
-                   (tbf/state '#hash((a . 1) (b . 1)) 0)))
-    (check-equal? (read-org-sbfs/state "((-1 2) (1 1))" #:headers #f)
-                  (list
-                   (tbf/state '#hash((x0 . -1) (x1 . 2)) 0)
-                   (tbf/state '#hash((x0 . 1) (x1 . 1)) 0)))))
-
-;;; Given a list of tbf/state, produces a sexp that Org-mode can
-;;; interpret as a table.
-;;;
-;;; All tbf/state in the list must have the same inputs.  The function
-;;; does not check this property.
-;;;
-;;; If #:headers is #f, does not print the names of the inputs of the
-;;; TBFs.  If #:headers is #t, the output starts by a list giving the
-;;; names of the variables, as well as the symbol 'θ to represent the
-;;; column giving the thresholds of the TBF.
-(define (print-org-tbfs/state tbfs #:headers [headers #t])
-  (define table (for/list ([tbf (in-list tbfs)])
-                  (append (hash-map (tbf/state-w tbf) (λ (_ w) w) #t)
-                          (list (tbf/state-θ tbf)))))
-  (if headers
-      (cons (append (hash-map (tbf/state-w (car tbfs)) (λ (x _) x) #t) '(θ))
-            table)
-      table))
-
-(module+ test
-  (test-case "print-org-tbfs/state"
-    (define tbfs (list (make-tbf/state '((a . 1) (b . 2)) 3)
-                       (make-tbf/state '((a . -2) (b . 1)) 1)))
-    (check-equal? (print-org-tbfs/state tbfs)
-                  '((a b θ) (1 2 3) (-2 1 1)))))
-
-;;; Like print-org-tbfs/state, but expects a list of SBFs.  The
-;;; thresholds are therefore not included in the output.
-;;;
-;;; All sbf/state in the list must have the same inputs.  The function
-;;; does not check this property.
-;;;
-;;; If #:headers is #f, does not print the names of the inputs of the
-;;; TBFs.  If #:headers is #t, the output starts by a list giving the
-;;; names of the variables.
-(define (print-org-sbfs/state sbfs #:headers [headers #t])
-  (define table (for/list ([sbf (in-list sbfs)])
-                  (hash-map (tbf/state-w sbf) (λ (_ w) w) #t)))
-  (if headers
-      (cons (hash-map (tbf/state-w (car sbfs)) (λ (x _) x) #t)
-            table)
-      table))
-
-(module+ test
-  (define sbfs (list (make-sbf/state '((a . 1) (b . 2)))
-                     (make-sbf/state '((a . -2) (b . 1)))))
-  (check-equal? (print-org-sbfs/state sbfs)
-                '((a b) (1 2) (-2 1)))
-  (check-equal? (print-org-sbfs/state sbfs #:headers #f)
-                '((1 2) (-2 1))))
-
-;;; Tabulates a list of tbf/state.
-;;;
-;;; As in the case of tbf-tabulate*, the result is a list of lists
-;;; giving the truth tables of the given TBFs.  The first elements of
-;;; each row give the values of the inputs, while the last elements
-;;; give the values of each function corresponding to the input.
-;;;
-;;; All the TBFs must have exactly the same inputs.  This function
-;;; does not check this property.
-;;;
-;;; If #:headers is #t, the output starts by a list giving the names
-;;; of the variables, and then the symbols 'fi, where i is the number
-;;; of the TBF in the list.
-(define (tbf/state-tabulate* tbfs #:headers [headers #t])
-  (define vars (hash-map (tbf/state-w (car tbfs)) (λ (x _) x) #t))
-  (tabulate-state* (map (curry apply-tbf/state) tbfs)
-                   (make-same-domains vars '(0 1))
-                   #:headers headers))
-
-(module+ test
-  (test-case "tbf/state-tabulate*"
-    (define tbfs (list (make-tbf/state '((a . 1) (b . 2)) 1)
-                       (make-tbf/state '((a . -2) (b . 3)) 1)))
-    (check-equal? (tbf/state-tabulate* tbfs)
-                  '((a b f1 f2)
-                    (0 0 0 0)
-                    (0 1 1 1)
-                    (1 0 0 0)
-                    (1 1 1 0)))))
-
-;;; Like tbf/state-tabulate*, but only tabulates a single TBF.
-(define (tbf/state-tabulate tbf #:headers [headers #t])
-  (tbf/state-tabulate* (list tbf) #:headers headers))
-
-(module+ test
-  (test-case "tbf/state-tabulate"
-    (define tbf (make-tbf/state '((a . -2) (b . 3)) 1))
-    (check-equal? (tbf/state-tabulate tbf)
-                  '((a b f1)
-                    (0 0 0)
-                    (0 1 1)
-                    (1 0 0)
-                    (1 1 0)))))
-
-;;; Given a truth table of a Boolean function, groups the lines by the
-;;; "number of activated inputs"—the number of inputs which are 1 in
-;;; the input vector.
-;;;
-;;; The truth table must not include the header line.
-(define (group-truth-table-by-nai tt)
-  (define sum (((curry foldl) +) 0))
-  (group-by (λ (row) (drop-right row 1))
-            tt
-            (λ (in1 in2) (= (sum in1) (sum in2)))))
-
-(module+ test
-  (test-case "group-truth-table-by-nai"
-    (check-equal? (group-truth-table-by-nai '((0 0 0 1)
-                                              (0 0 1 1)
-                                              (0 1 0 0)
-                                              (0 1 1 1)
-                                              (1 0 0 0)
-                                              (1 0 1 0)
-                                              (1 1 0 1)
-                                              (1 1 1 0)))
-                  '(((0 0 0 1))
-                    ((0 0 1 1) (0 1 0 0) (1 0 0 0))
-                    ((0 1 1 1) (1 0 1 0) (1 1 0 1))
-                    ((1 1 1 0))))))
-
-;;; A TBN is a network form mapping variables to tbf/state.
-;;;
-;;; The tbf/state must only reference variables appearing in the
-;;; network.  This contract does not check this condition.
-(define tbn? (hash/c variable? tbf/state?))
-
-;;; Builds a TBN from a list of pairs (variable, tbf/state).
-(define make-tbn make-immutable-hash)
-
-(module+ test
-  (test-case "make-tbn"
-    (define tbf-not (make-tbf/state '((a . -1)) -1))
-    (define tbf-id (make-sbf/state '((a . 1))))
-    (check-equal? (make-tbn `((a . ,tbf-not) (b . ,tbf-id)))
-                  (hash 'a (tbf/state '#hash((a . -1)) -1)
-                        'b (tbf/state '#hash((a . 1)) 0)))))
-
-;;; A SBN is a network form mapping variables to sbf/state.
-;;;
-;;; The tbf/state must only reference variables appearing in the
-;;; network.  This contract does not check this condition.
-(define sbn? (hash/c variable? sbf/state?))
-
-;;; Builds an SBN from a list of pairs (variable, sbf/state).
-(define make-sbn make-immutable-hash)
-
-(module+ test
-  (test-case "make-sbn"
-    (define sbf1 (make-sbf/state '((a . -1))))
-    (define sbf2 (make-sbf/state '((a . 1))))
-    (check-equal? (make-sbn `((a . ,sbf1) (b . ,sbf2)))
-                  (hash 'a (tbf/state '#hash((a . -1)) 0)
-                        'b (tbf/state '#hash((a . 1)) 0)))))
-
-;;; Constructs a network from a network form defining a TBN.
-(define (tbn->network tbn)
-  (make-01-network (for/hash ([(var tbf) (in-hash tbn)])
-                     (values var ((curry apply-tbf/state) tbf)))))
-
-(module+ test
-  (test-case "tbn->network"
-    (define tbn (make-tbn `((a . ,(make-sbf/state '((b . 1))))
-                            (b . ,(make-tbf/state '((a . -1)) -1)))))
-    (define n (tbn->network tbn))
-    (define s1 (hash 'a 0 'b 0))
-    (check-equal? (update n s1 '(a b))
-                  (hash 'a 0 'b 1))
-    (check-equal? (network-domains n) #hash((a . (0 1)) (b . (0 1))))
-
-    (define sbn (make-sbn `((a . ,(make-sbf/state '((b . -1))))
-                            (b . ,(make-sbf/state '((a . 1)))))))
-    (define sn (tbn->network sbn))
-    (define s2 (hash 'a 1 'b 1))
-    (check-equal? (update sn s2 '(a b))
-                  (hash 'a 0 'b 1))
-    (check-equal? (network-domains sn) #hash((a . (0 1)) (b . (0 1))))))
-
-;;; A helper function for read-org-tbn and read-org-sbn.  It reads a
-;;; TBN from an Org-mode sexp containing a list of lists of numbers.
-;;; As in lists->tbfs/state, the last element of each list is taken to
-;;; be the threshold of the TBFs, and the rest of the elements are
-;;; taken to be the weights.
-;;;
-;;; As in read-org-tbfs/state, if headers is #t, the names of the
-;;; variables to appear as the inputs of the TBF are taken from the
-;;; first list.  The last element of this list is discarded.
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-;;;
-;;; If func-names is #t, the first element in every row except the
-;;; first one, are taken to be the name of the variable to which the
-;;; TBF should be associated.  If func-names is #f, the functions are
-;;; assigned to variables in alphabetical order.
-;;;
-;;; func-names cannot be #t if headers is #f.  The function does not
-;;; check this condition.
-(define (parse-org-tbn sexp
-                       #:headers [headers #t]
-                       #:func-names [func-names #t])
-  (cond
-    [(eq? func-names #t)
-     (define-values (vars rows) (multi-split-at sexp 1))
-     (define tbfs (lists->tbfs/state rows #:headers headers))
-     (for/hash ([tbf (in-list tbfs)] [var (in-list (cdr vars))])
-       (values (car var) tbf))]
-    [else
-     (define tbfs (lists->tbfs/state sexp #:headers headers))
-     (define vars (hash-map (tbf/state-w (car tbfs)) (λ (x _) x) #t))
-     (for/hash ([tbf (in-list tbfs)] [var (in-list vars)])
-       (values var tbf))]))
-
-;;; Reads a TBN from an Org-mode string containing a sexp, containing
-;;; a list of lists of numbers.  As in lists->tbfs/state, the last
-;;; element of each list is taken to be the threshold of the TBFs, and
-;;; the rest of the elements are taken to be the weights.
-;;;
-;;; As in read-org-tbfs/state, if headers is #t, the names of the
-;;; variables to appear as the inputs of the TBF are taken from the
-;;; first list.  The last element of this list is discarded.
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-;;;
-;;; If func-names is #t, the first element in every row except the
-;;; first one, are taken to be the name of the variable to which the
-;;; TBF should be associated.  If func-names is #f, the functions are
-;;; assigned to variables in alphabetical order.
-;;;
-;;; func-names cannot be #t if headers is #f.  The function does not
-;;; check this condition.
-(define (read-org-tbn str
-                      #:headers [headers #t]
-                      #:func-names [func-names #t])
-  (parse-org-tbn (read-org-sexp str)
-                 #:headers headers
-                 #:func-names func-names))
-
-(module+ test
-  (test-case "read-org-tbn, parse-org-tbn"
-    (check-equal? (read-org-tbn "((\"-\" \"x\" \"y\" \"θ\") (\"y\" -1 0 -1) (\"x\" 0 -1 -1))")
-                  (hash
-                   'x
-                   (tbf/state '#hash((x . 0) (y . -1)) -1)
-                   'y
-                   (tbf/state '#hash((x . -1) (y . 0)) -1)))
-    (check-equal? (read-org-tbn "((\"x\" \"y\" \"θ\") (-1 0 -1) (0 -1 -1))" #:func-names #f)
-                  (hash
-                   'x
-                   (tbf/state '#hash((x . -1) (y . 0)) -1)
-                   'y
-                   (tbf/state '#hash((x . 0) (y . -1)) -1)))
-    (check-equal? (read-org-tbn "((-1 0 -1) (0 -1 -1))" #:headers #f #:func-names #f)
-                  (hash
-                   'x0
-                   (tbf/state '#hash((x0 . -1) (x1 . 0)) -1)
-                   'x1
-                   (tbf/state '#hash((x0 . 0) (x1 . -1)) -1)))))
-
-;;; Like read-org-tbn, but reads an SBN from an Org-mode string
-;;; containing a sexp, containing a list of lists of numbers.
-;;;
-;;; As in read-org-sbfs/state, if headers is #t, the names of the
-;;; variables to appear as the inputs of the SBF are taken from the
-;;; first list.  The last element of this list is discarded.
-;;; If headers is #f, the names of the variables are generated as xi,
-;;; where i is the index of the variable.
-;;;
-;;; If func-names is #t, the first element in every row except the
-;;; first one, are taken to be the name of the variable to which the
-;;; TBF should be associated.  If func-names is #f, the functions are
-;;; assigned to variables in alphabetical order.
-;;;
-;;; func-names cannot be #t if headers is #f.  The function does not
-;;; check this condition.
-(define (read-org-sbn str
-                      #:headers [headers #t]
-                      #:func-names [func-names #t])
-  (define sexp (read-org-sexp str))
-  ;; Inject the 0 thresholds into the rows of the sexp we have just read.
-  (define (inject-0 rows) (for/list ([row (in-list rows)]) (append row '(0))))
-  (define sexp-ready (if headers
-                         (cons (car sexp) (inject-0 (cdr sexp)))
-                         (inject-0 sexp)))
-  (parse-org-tbn sexp-ready #:headers headers #:func-names func-names))
-
-(module+ test
-  (test-case "read-org-sbn, parse-org-tbn"
-    (check-equal? (read-org-sbn "((\"-\" \"x\" \"y\") (\"y\" -1 0) (\"x\" 0 -1))")
-                  (hash
-                   'x
-                   (tbf/state '#hash((x . 0) (y . -1)) 0)
-                   'y
-                   (tbf/state '#hash((x . -1) (y . 0)) 0)))
-    (check-equal? (read-org-sbn "((\"x\" \"y\") (-1 0) (0 -1))" #:func-names #f)
-                  (hash
-                   'x
-                   (tbf/state '#hash((x . -1) (y . 0)) 0)
-                   'y
-                   (tbf/state '#hash((x . 0) (y . -1)) 0)))
-    (check-equal? (read-org-sbn "((-1 0) (0 -1))" #:headers #f #:func-names #f)
-                  (hash
-                   'x0
-                   (tbf/state '#hash((x0 . -1) (x1 . 0)) 0)
-                   'x1
-                   (tbf/state '#hash((x0 . 0) (x1 . -1)) 0)))))
-
-;;; A shortcut for building the state graphs of TBN.
-(define build-tbn-state-graph
-  (compose pretty-print-state-graph
-           build-full-state-graph
-           make-syn-dynamics
-           tbn->network))
-
-;;; Checks whether a TBN is normalized: whether all of the functions
-;;; have the same inputs, and whether these inputs are exactly the
-;;; variables of the TBN.
-(define (normalized-tbn? tbn)
-  (define tbn-vars (hash-keys tbn))
-  (for/and ([tbf (in-list (hash-values tbn))])
-    (set=? tbn-vars (hash-keys (tbf/state-w tbf)))))
-
-(module+ test
-  (test-case "normalized-tbn?"
-    (check-false (normalized-tbn?
-                  (make-tbn `((a . ,(make-sbf/state '((b . 1))))
-                              (b . ,(make-tbf/state '((a . -1)) -1))))))
-    (check-true (normalized-tbn?
-                 (make-tbn `((a . ,(make-sbf/state '((a . 1) (b . -1))))
-                             (b . ,(make-tbf/state '((a . -1) (b . 1)) -1))))))))
-
-;;; Normalizes a TBN.
-;;;
-;;; For every TBF, removes the inputs that are not in the variables of
-;;; the TBN, and adds missing inputs with 0 weight.
-(define (normalize-tbn tbn)
-  (define vars-0 (for/hash ([(x _) (in-hash tbn)]) (values x 0)))
-  (define (normalize-tbf tbf)
-    ;; Only keep the inputs which are also the variables of tbn.
-    (define w-pruned (hash-intersect tbn (tbf/state-w tbf)
-                                     #:combine (λ (_ w) w)))
-    ;; Put in the missing inputs with weight 0.
-    (define w-complete (hash-union vars-0 w-pruned #:combine (λ (_ w) w)))
-    (tbf/state w-complete (tbf/state-θ tbf)))
-  (for/hash ([(x tbf) (in-hash tbn)]) (values x (normalize-tbf tbf))))
-
-(module+ test
-  (test-case "normalize-tbn"
-    (check-equal? (normalize-tbn
-                   (hash 'a (make-sbf/state '((b . 1) (c . 3)))
-                         'b (make-tbf/state '((a . -1)) -1)))
-                  (hash
-                   'a
-                   (tbf/state '#hash((a . 0) (b . 1)) 0)
-                   'b
-                   (tbf/state '#hash((a . -1) (b . 0)) -1)))))
-
-;;; Compacts (and denormalizes) a TBF by removing all inputs which
-;;; are 0.
-(define (compact-tbf tbf)
-  (tbf/state
-   (for/hash ([(k v) (in-hash (tbf/state-w tbf))]
-              #:unless (zero? v))
-     (values k v))
-   (tbf/state-θ tbf)))
-
-(module+ test
-  (test-case "compact-tbf"
-    (check-equal? (compact-tbf (tbf/state (hash 'a 0 'b 1 'c 2 'd 0) 2))
-                  (tbf/state '#hash((b . 1) (c . 2)) 2))))
-
-;;; Compacts a TBN by removing all inputs which are 0 or which are not
-;;; variables of the network.
-(define (compact-tbn tbn)
-  (define (remove-0-non-var tbf)
-    (tbf/state
-     (for/hash ([(x w) (in-hash (tbf/state-w tbf))]
-                #:when (hash-has-key? tbn x)
-                #:unless (zero? w))
-       (values x w))
-     (tbf/state-θ tbf)))
-  (for/hash ([(x tbf) (in-hash tbn)])
-    (values x (remove-0-non-var tbf))))
-
-(module+ test
-  (test-case "compact-tbn"
+  (test-case "random-boolean-network"
     (check-equal?
-     (compact-tbn (hash 'a (tbf/state (hash 'a 0 'b 1 'c 3 'd 0) 0)
-                        'b (tbf/state (hash 'a -1 'b 1) -1)))
-     (hash
-      'a
-      (tbf/state '#hash((b . 1)) 0)
-      'b
-      (tbf/state '#hash((a . -1) (b . 1)) -1)))))
+     (tabulate-network+headers (random-boolean-network '(x y z)))
+     '((x y z f-x f-y f-z)
+       (#f #f #f #t #t #t)
+       (#f #f #t #f #f #f)
+       (#f #t #f #t #t #t)
+       (#f #t #t #f #t #f)
+       (#t #f #f #t #t #t)
+       (#t #f #t #f #t #f)
+       (#t #t #f #f #f #t)
+       (#t #t #t #t #t #f)))))
 
-;;; Given TBN, produces a sexp containing the description of the
-;;; functions of the TBN that Org-mode can interpret as a table.
-;;;
-;;; Like print-org-tbfs/state, if #:headers is #f, does not print the
-;;; names of the inputs of the TBFs.  If #:headers is #t, the output
-;;; starts by a list giving the names of the variables, as well as the
-;;; symbol 'θ to represent the column giving the thresholds of the
-;;; TBF.
-;;;
-;;; If #:func-names is #t, the first column of the table gives the
-;;; variable which the corresponding TBF updates.
-;;;
-;;; If both #:func-names and #:headers are #t, the first cell of the
-;;; first column contains the symbol '-.
-(define (print-org-tbn tbn
-                       #:headers [headers #t]
-                       #:func-names [func-names #t])
-  (define ntbn (normalize-tbn tbn))
-  (define vars-tbfs (hash-map ntbn (λ (x tbf) (cons x tbf)) #t))
-  (define tbfs (map cdr vars-tbfs))
-  (define tbfs-table (print-org-tbfs/state tbfs #:headers headers))
-  (cond
-    [(eq? func-names #t)
-     (define vars (map car vars-tbfs))
-     (define col-1 (if headers (cons '- vars) vars))
-     (for/list ([var (in-list col-1)] [row (in-list tbfs-table)])
-       (cons var row))]
-    [else
-     tbfs-table]))
+(: random-boolean-network/n (-> Positive-Integer (Network Boolean)))
+(define (random-boolean-network/n n)
+  (random-boolean-network (for/list : (Listof Variable)
+                                    ([i (in-range n)])
+                            (string->symbol (format "x~a" i)))))
 
 (module+ test
-  (test-case "print-org-tbn"
-    (define tbn (make-tbn `((a . ,(make-sbf/state '((b . 1))))
-                            (b . ,(make-tbf/state '((a . -1)) -1)))))
-    (check-equal? (print-org-tbn tbn)
-                  '((- a b θ) (a 0 1 0) (b -1 0 -1)))))
-
-;;; Given an SBN, produces a sexp containing the description of the
-;;; functions of the SBN that Org-mode can interpret as a table.
-;;; This function is therefore very similar to print-org-tbn.
-;;;
-;;; Like print-org-tbfs/state, if #:headers is #f, does not print the
-;;; names of the inputs of the TBFs.  If #:headers is #t, the output
-;;; starts by a list giving the names of the variables.
-;;;
-;;; If #:func-names is #t, the first column of the table gives the
-;;; variable which the corresponding TBF updates.
-;;;
-;;; If both #:func-names and #:headers are #t, the first cell of the
-;;; first column contains the symbol '-.
-(define (print-org-sbn sbn
-                       #:headers [headers #t]
-                       #:func-names [func-names #t])
-  (define tab (print-org-tbn sbn #:headers headers #:func-names func-names))
-  (define-values (tab-no-θ _) (multi-split-at
-                               tab
-                               (- (length (car tab)) 1)))
-  tab-no-θ)
-
-(module+ test
-  (test-case "print-org-sbn"
-    (define sbn (hash
-                 'a
-                 (tbf/state (hash 'b 2) 0)
-                 'b
-                 (tbf/state (hash 'a 2) 0)))
-    (check-equal? (print-org-sbn sbn)
-                  '((- a b) (a 0 2) (b 2 0)))))
-
-;;; Given a TBN, constructs its interaction graph.  The nodes of this
-;;; graph are labeled with pairs (variable name . threshold), while
-;;; the edges are labelled with the weights.
-;;;
-;;; If #:zero-edges is #t, the edges with zero weights will appear in
-;;; the interaction graph.
-(define (tbn-interaction-graph tbn
-                               #:zero-edges [zero-edges #t])
-  (define ntbn (normalize-tbn tbn))
-  (define ig (weighted-graph/directed
-              (if zero-edges
-                  (for*/list ([(tar tbf) (in-hash ntbn)]
-                              [(src w) (in-hash (tbf/state-w tbf))])
-                    (list w src tar))
-                  (for*/list ([(tar tbf) (in-hash ntbn)]
-                              [(src w) (in-hash (tbf/state-w tbf))]
-                              #:unless (zero? w))
-                    (list w src tar)))))
-  (update-graph ig #:v-func (λ (x) (cons x (tbf/state-θ (hash-ref ntbn x))))))
-
-(module+ test
-  (test-case "tbn-interaction-graph"
-    (define tbn (make-tbn `((a . ,(make-sbf/state '((b . 1))))
-                            (b . ,(make-tbf/state '((a . -1)) -1)))))
-    (check-equal? (graphviz (tbn-interaction-graph tbn))
-                  "digraph G {\n\tnode0 [label=\"'(b . -1)\\n\"];\n\tnode1 [label=\"'(a . 0)\\n\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [label=\"0\"];\n\t\tnode1 -> node1 [label=\"0\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"1\"];\n\t\tnode1 -> node0 [label=\"-1\"];\n\t}\n}\n")
-    (check-equal? (graphviz (tbn-interaction-graph tbn #:zero-edges #f))
-                  "digraph G {\n\tnode0 [label=\"'(b . -1)\\n\"];\n\tnode1 [label=\"'(a . 0)\\n\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"1\"];\n\t\tnode1 -> node0 [label=\"-1\"];\n\t}\n}\n")))
-
-;;; Pretty prints the node labels of the interaction graph of a TBN.
-(define (pretty-print-tbn-interaction-graph ig)
-  (update-graph ig #:v-func (match-lambda
-                              [(cons var weight) (~a var ":" weight)])))
-
-(module+ test
-  (test-case "pretty-print-tbn-interaction-graph"
-    (define tbn (make-tbn `((a . ,(make-sbf/state '((b . 1))))
-                            (b . ,(make-tbf/state '((a . -1)) -1)))))
-    (check-equal? (graphviz (pretty-print-tbn-interaction-graph (tbn-interaction-graph tbn)))
-                  "digraph G {\n\tnode0 [label=\"b:-1\"];\n\tnode1 [label=\"a:0\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node0 [label=\"0\"];\n\t\tnode1 -> node1 [label=\"0\"];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node1 [label=\"1\"];\n\t\tnode1 -> node0 [label=\"-1\"];\n\t}\n}\n")))
-
-;;; Given an SBN, constructs its interaction graph.  As in
-;;; tbn-interaction-graph, the nodes of this graph are labeled with
-;;; the variable names, while the edges are labelled with the weights.
-;;;
-;;; If #:zero-edges is #t, the edges with zero weights will appear in
-;;; the interaction graph.
-(define (sbn-interaction-graph sbn
-                               #:zero-edges [zero-edges #t])
-  (update-graph (tbn-interaction-graph sbn #:zero-edges zero-edges)
-                #:v-func (match-lambda
-                           [(cons var _) var])))
-
-(module+ test
-  (test-case "sbn-interaction-graph"
-    (define sbn (hash
-                 'a
-                 (tbf/state (hash 'b 2) 0)
-                 'b
-                 (tbf/state (hash 'a 2) 0)))
-    (check-equal? (graphviz (sbn-interaction-graph sbn))
-                  "digraph G {\n\tnode0 [label=\"b\"];\n\tnode1 [label=\"a\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t\tnode0 -> node1 [label=\"2\"];\n\t\tnode0 -> node0 [label=\"0\"];\n\t\tnode1 -> node1 [label=\"0\"];\n\t}\n\tsubgraph D {\n\t}\n}\n")))
+  (test-case "random-boolean-network/n"
+    (check-equal?
+     (tabulate-network+headers (random-boolean-network/n 3))
+     '((x0 x1 x2 f-x0 f-x1 f-x2)
+       (#f #f #f #f #t #f)
+       (#f #f #t #f #f #t)
+       (#f #t #f #t #f #f)
+       (#f #t #t #f #t #t)
+       (#t #f #f #t #t #t)
+       (#t #f #t #t #f #t)
+       (#t #t #f #t #t #f)
+       (#t #t #t #t #f #t)))))
diff --git a/scribblings/networks.scrbl b/scribblings/networks.scrbl
index 4c1530c..ea2ed86 100644
--- a/scribblings/networks.scrbl
+++ b/scribblings/networks.scrbl
@@ -4,7 +4,7 @@
 	  	     graph
 		     (only-in typed/graph Graph)
 		     (only-in racket/class send)
-		     (submod "../networks.rkt" typed)
+		     "../networks.rkt"
 		     "../utils.rkt"
 		     "../functions.rkt"
 		     "../dynamics.rkt"))
@@ -13,7 +13,7 @@
   (parameterize ([sandbox-output 'string]
   		 [sandbox-error-output 'string]
 		 [sandbox-memory-limit 50])
-   (make-evaluator 'typed/racket #:requires '((submod "networks.rkt" typed)))))
+   (make-evaluator 'typed/racket #:requires '("networks.rkt"))))
 
 @(define-syntax-rule (ex . args)
   (examples #:eval networks-evaluator . args))
@@ -26,7 +26,7 @@
 
 @title[#:tag "networks"]{dds/networks: Formal Dynamical Networks}
 
-@defmodule[(submod dds/networks typed)]
+@defmodule[dds/networks]
 
 This module provides definitions for and analysing network models.  A network
 is a set of variables which are updated according to their corresponding update
@@ -944,8 +944,3 @@ to @tt{xk}, where @italic{k = n - 1}.
 @ex[
 (tabulate-network+headers (random-boolean-network/n 3))
 ]}
-
-@section{TBF/TBN and SBF/SBN}
-
-This section defines threshold Boolean functions (TBF) and networks (TBN), as
-well as sign Boolean functions (SBF) and networks (SBN).