cpsa-4.4.4: tst/hull-alt.tst

(herald hull-alt (bound 9))

(comment "CPSA 4.4.4")
(comment "All input read from tst/hull-alt.scm")
(comment "Strand count bounded at 9")

(defprotocol wonthull2 basic
  (defrole init
    (vars (a name) (n r r-0 r-1 text))
    (trace (send (cat (enc n r (pubk a)) (enc r-0 n (pubk a))))
      (recv (enc "okay" n r-1 (pubk a))))
    (non-orig (privk a))
    (uniq-orig n))
  (defrole resp
    (vars (a name) (y1 y2 y3 text))
    (trace (recv (enc y1 y2 (pubk a)))
      (send (enc "okay" y3 y1 (pubk a)))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton wonthull2
  (vars (n r r-0 r-1 text) (a name))
  (defstrand init 2 (n n) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (non-orig (privk a))
  (uniq-orig n)
  (traces
    ((send (cat (enc n r (pubk a)) (enc r-0 n (pubk a))))
      (recv (enc "okay" n r-1 (pubk a)))))
  (label 0)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 r-1 y3 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (added-strand resp 2) r-0 (0 1)
    (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
  (strand-map 0)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-1 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a)))))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull2
  (vars (n r r-0 r-1 y3 text) (a name))
  (defstrand init 2 (n n) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 n) (y2 r) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1) (enc n r (pubk a))
    (enc r-0 n (pubk a)))
  (strand-map 0)
  (traces
    ((send (cat (enc n r (pubk a)) (enc r-0 n (pubk a))))
      (recv (enc "okay" n r-1 (pubk a))))
    ((recv (enc n r (pubk a))) (send (enc "okay" y3 n (pubk a)))))
  (label 2)
  (parent 0)
  (seen 5)
  (seen-ops
    (5
      (operation nonce-test (added-strand resp 2) r-0 (0 1)
        (enc "okay" y3 r-0 (pubk a)) (enc r-0 r (pubk a))
        (enc r-0 r-0 (pubk a))) (strand-map 0 2)))
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (r y3 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 y3) (r-1 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (r-0 y3) (r-1 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc y3 r (pubk a))
    (enc y3 y3 (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 3)
  (parent 1)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 r-1 y3 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (added-strand resp 2) r-0 (0 1)
    (enc "okay" y3 r-0 (pubk a)) (enc r-0 r (pubk a))
    (enc r-0 r-0 (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-1 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a)))
      (send (enc "okay" r-0 r-0 (pubk a)))))
  (label 4)
  (parent 1)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 r-1 y3 y3-0 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (added-strand resp 2) r-0 (0 1)
    (enc "okay" y3 r-0 (pubk a)) (enc r-0 r (pubk a))
    (enc r-0 r-0 (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-1 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3-0 r-0 (pubk a)))))
  (label 5)
  (parent 1)
  (seen 10)
  (seen-ops
    (10
      (operation nonce-test (added-strand resp 2) r-0 (0 1)
        (enc "okay" y3 r-0 (pubk a)) (enc "okay" y3-0 r-0 (pubk a))
        (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
      (strand-map 0 1 3)))
  (unrealized (0 1))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 y3 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 r-0) (r-1 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 r) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (n y3) (r-1 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc r-0 y3 (pubk a))
    (enc y3 r (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc r-0 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 r (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 6)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((a a) (n y3) (r r) (r-0 r-0) (r-1 y3))))
  (origs (y3 (0 0))))

(defskeleton wonthull2
  (vars (n r r-0 r-1 y3 text) (a name))
  (defstrand init 2 (n n) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 n) (y2 r) (y3 y3) (a a))
  (defstrand resp 2 (y1 n) (y2 r) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1)
    (enc "okay" y3 n (pubk a)) (enc n r (pubk a)) (enc r-0 n (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (cat (enc n r (pubk a)) (enc r-0 n (pubk a))))
      (recv (enc "okay" n r-1 (pubk a))))
    ((recv (enc n r (pubk a))) (send (enc "okay" y3 n (pubk a))))
    ((recv (enc n r (pubk a))) (send (enc "okay" r-0 n (pubk a)))))
  (label 7)
  (parent 2)
  (seen 13)
  (seen-ops
    (13
      (operation nonce-test (added-strand resp 2) r-0 (0 1)
        (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
        (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
      (strand-map 0 2 3)))
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (r y3 y3-0 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 y3-0) (r-1 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization separated y3-0)
  (strand-map 0 1)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc y3-0 y3 (pubk a))))
      (recv (enc "okay" y3 y3-0 (pubk a))))
    ((recv (enc y3-0 y3 (pubk a)))
      (send (enc "okay" y3 y3-0 (pubk a)))))
  (label 8)
  (parent 3)
  (realized)
  (shape)
  (maps ((0) ((a a) (n y3) (r r) (r-0 y3-0) (r-1 y3-0))))
  (origs (y3 (0 0))))

(defskeleton wonthull2
  (vars (r r-0 y3 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (contracted (r-1 r-0)) r-0 (0 1)
    (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
    (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a)))
      (send (enc "okay" r-0 r-0 (pubk a)))))
  (label 9)
  (parent 4)
  (seen 3)
  (seen-ops
    (3 (operation generalization deleted (1 0)) (strand-map 0 2)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 r-1 y3 y3-0 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (added-strand resp 2) r-0 (0 1)
    (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
    (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-1 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3-0 r-0 (pubk a)))))
  (label 10)
  (parent 4)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (r y3 y3-0 text) (a name))
  (defstrand init 2 (n y3-0) (r r) (r-0 y3-0) (r-1 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 r) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3-0)
  (operation nonce-test (contracted (r-0 y3-0) (r-1 y3-0)) y3-0 (0 1)
    (enc "okay" y3 y3-0 (pubk a)) (enc "okay" y3-0 y3-0 (pubk a))
    (enc y3-0 r (pubk a)) (enc y3-0 y3-0 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc y3-0 r (pubk a)) (enc y3-0 y3-0 (pubk a))))
      (recv (enc "okay" y3-0 y3-0 (pubk a))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3 y3-0 (pubk a))))
    ((recv (enc y3-0 r (pubk a)))
      (send (enc "okay" y3-0 y3-0 (pubk a)))))
  (label 11)
  (parent 5)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (r y3 y3-0 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 y3) (r-1 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 r) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (r-0 y3) (r-1 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 r (pubk a)) (enc y3 y3 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 r (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 12)
  (parent 5)
  (seen 3)
  (seen-ops
    (3 (operation generalization deleted (2 0)) (strand-map 0 1)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 r-1 y3 y3-0 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-1) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (added-strand resp 2) r-0 (0 1)
    (enc "okay" y3 r-0 (pubk a)) (enc "okay" y3-0 r-0 (pubk a))
    (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-1 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3-0 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" r-0 r-0 (pubk a)))))
  (label 13)
  (parent 5)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 y3 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (contracted (n r-0) (r-1 r-0)) r-0 (0 1)
    (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
    (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" r-0 r-0 (pubk a)))))
  (label 14)
  (parent 7)
  (seen 17)
  (seen-ops
    (17 (operation generalization deleted (1 0)) (strand-map 0 2)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 y3 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 r-0) (r-1 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 r) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 r) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (n y3) (r-1 y3)) y3 (0 1)
    (enc "okay" r-0 y3 (pubk a)) (enc "okay" y3 y3 (pubk a))
    (enc r-0 y3 (pubk a)) (enc y3 r (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc r-0 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 r (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 r (pubk a))) (send (enc "okay" r-0 y3 (pubk a)))))
  (label 15)
  (parent 7)
  (seen 6)
  (seen-ops
    (6 (operation generalization deleted (2 0)) (strand-map 0 1)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 y3 y3-0 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (contracted (r-1 r-0)) r-0 (0 1)
    (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
    (enc "okay" y3-0 r-0 (pubk a)) (enc r-0 r (pubk a))
    (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2 3)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3-0 r-0 (pubk a)))))
  (label 16)
  (parent 10)
  (seen 12)
  (seen-ops
    (12 (operation generalization deleted (1 0)) (strand-map 0 2 3)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r y3 text) (a name))
  (defstrand init 2 (n y3) (r r) (r-0 y3) (r-1 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 r) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (1 0))
  (strand-map 0 2)
  (traces
    ((send (cat (enc y3 r (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 r (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 17)
  (parent 11)
  (seen 6)
  (seen-ops
    (6 (operation generalization separated y3-0) (strand-map 0 1)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (r r-0 y3 y3-0 text) (a name))
  (defstrand init 2 (n r-0) (r r) (r-0 r-0) (r-1 r-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 r-0) (y2 r) (y3 r-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig r-0)
  (operation nonce-test (contracted (r-1 r-0)) r-0 (0 1)
    (enc "okay" r-0 r-0 (pubk a)) (enc "okay" y3 r-0 (pubk a))
    (enc "okay" y3-0 r-0 (pubk a)) (enc r-0 r (pubk a))
    (enc r-0 r-0 (pubk a)))
  (strand-map 0 1 2 3)
  (traces
    ((send (cat (enc r-0 r (pubk a)) (enc r-0 r-0 (pubk a))))
      (recv (enc "okay" r-0 r-0 (pubk a))))
    ((recv (enc r-0 r-0 (pubk a))) (send (enc "okay" y3 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" y3-0 r-0 (pubk a))))
    ((recv (enc r-0 r (pubk a))) (send (enc "okay" r-0 r-0 (pubk a)))))
  (label 18)
  (parent 13)
  (seen 14)
  (seen-ops
    (14 (operation generalization deleted (1 0)) (strand-map 0 2 3)))
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")