#lang 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 . #f) (y . #t) (z . #f))\"];\n\tnode1 [label=\"'#hash((x . #t) (y . #f) (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 -> node3 [label=\"'(x y z)\"];\n\t\tnode1 -> node2 [label=\"'(x y z)\"];\n\t\tnode2 -> node0 [label=\"'(x y z)\"];\n\t\tnode3 -> node1 [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 . #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 [];\n\t\tnode2 -> 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 . #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 [];\n\t\tnode1 -> node3 [];\n\t\tnode2 -> node1 [];\n\t\tnode3 -> node0 [];\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 . #f) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode2 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode4 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\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 -> node1 [];\n\t\tnode1 -> node3 [];\n\t\tnode2 -> node7 [];\n\t\tnode3 -> node5 [];\n\t\tnode4 -> node5 [];\n\t\tnode5 -> node2 [];\n\t\tnode6 -> node0 [];\n\t\tnode7 -> node3 [];\n\t}\n}\n"))
    (test-case "build-full-state-graph/annotated"
      (check-equal? (graphviz sg/an)
                    "digraph G {\n\tnode0 [label=\"'#hash((x . #f) (y . #t) (z . #t))\"];\n\tnode1 [label=\"'#hash((x . #f) (y . #f) (z . #t))\"];\n\tnode2 [label=\"'#hash((x . #t) (y . #f) (z . #f))\"];\n\tnode3 [label=\"'#hash((x . #f) (y . #t) (z . #f))\"];\n\tnode4 [label=\"'#hash((x . #t) (y . #f) (z . #t))\"];\n\tnode5 [label=\"'#hash((x . #t) (y . #t) (z . #f))\"];\n\tnode6 [label=\"'#hash((x . #t) (y . #t) (z . #t))\"];\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 -> node1 [label=\"'(z y x)\"];\n\t\tnode1 -> node2 [label=\"'(z y x)\"];\n\t\tnode2 -> node5 [label=\"'(z y x)\"];\n\t\tnode3 -> node7 [label=\"'(z y x)\"];\n\t\tnode4 -> node5 [label=\"'(z y x)\"];\n\t\tnode5 -> node3 [label=\"'(z y x)\"];\n\t\tnode6 -> node0 [label=\"'(z y x)\"];\n\t\tnode7 -> node2 [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:#t z:#t\"];\n\tnode3 [label=\"x:#t y:#f 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 -> node1 [];\n\t\tnode3 -> node4 [];\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:1 y:1 z:1\"];\n\tnode3 [label=\"x:0 y:0 z:1\"];\n\tnode4 [label=\"x:1 y:0 z:1\"];\n\tnode5 [label=\"x:0 y:1 z:0\"];\n\tnode6 [label=\"x:1 y:1 z:0\"];\n\tnode7 [label=\"x:0 y:0 z:0\"];\n\tsubgraph U {\n\t\tedge [dir=none];\n\t}\n\tsubgraph D {\n\t\tnode0 -> node6 [];\n\t\tnode1 -> node3 [];\n\t\tnode2 -> node1 [];\n\t\tnode3 -> node0 [];\n\t\tnode4 -> node6 [];\n\t\tnode5 -> node7 [];\n\t\tnode6 -> node5 [];\n\t\tnode7 -> node0 [];\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)))))