(herald "Subsort constraint test protocol"
  (comment "First, third, and fourth skeletons should have a shape,"
    "second should be dead."))
(comment "CPSA 3.4.0")
(comment "All input read from subsort_test.scm")

Trees: 0 2 3 5.

Tree 0.

1 0 
(defprotocol subsorttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)))

Item 0, Child: 1.

n2 (cat n1 (enc n1 n2 k)) ((n1 n1) (n2 n2) (k k)) init subsorttest 0
(defskeleton subsorttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0.

n1 (cat n1 (enc n1 n1 k)) ((n1 n1) (n2 n1) (k k)) init subsorttest 1 (realized) 
(defskeleton subsorttest
  (vars (n1 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n1) (k k))
  (non-orig k)
  (uniq-orig n1)
  (operation nonce-test (displaced 1 0 init 1) n2 (0 1) (enc n1 n2 k))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((n1 n1) (n2 n1) (k k))))
  (origs (n1 (0 0))))

Tree 2.

2 
(defprotocol subsorttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)))

Item 2.

n2 (cat n1 (enc n1 n2 k)) ((n1 n1) (n2 n2) (k k)) init subsorttest 2
(defskeleton subsorttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (non-orig k)
  (subsort (A n1) (B n2))
  (uniq-orig n1 n2)
  (label 2)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "empty cohort"))

Tree 3.

4 3 
(defprotocol subsorttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)))

Item 3, Child: 4.

n2 (cat n1 (enc n1 n2 k)) ((n1 n1) (n2 n2) (k k)) init subsorttest 3
(defskeleton subsorttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (non-orig k)
  (subsort (A n1))
  (uniq-orig n1 n2)
  (label 3)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 4, Parent: 3.

n1 (cat n1 (enc n1 n1 k)) ((n1 n1) (n2 n1) (k k)) init subsorttest 4 (realized) 
(defskeleton subsorttest
  (vars (n1 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n1) (k k))
  (non-orig k)
  (subsort (A n1))
  (uniq-orig n1)
  (operation nonce-test (displaced 1 0 init 1) n2 (0 1) (enc n1 n2 k))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((n1 n1) (n2 n1) (k k))))
  (origs (n1 (0 0))))

Tree 5.

6 5 
(defprotocol subsorttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)))

Item 5, Child: 6.

n2 (cat n1 (enc n1 n2 k)) ((n1 n1) (n2 n2) (k k)) init subsorttest 5
(defskeleton subsorttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (non-orig k)
  (subsort (A n1 n2))
  (uniq-orig n1 n2)
  (label 5)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 6, Parent: 5.

n1 (cat n1 (enc n1 n1 k)) ((n1 n1) (n2 n1) (k k)) init subsorttest 6 (realized) 
(defskeleton subsorttest
  (vars (n1 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n1) (k k))
  (non-orig k)
  (subsort (A n1))
  (uniq-orig n1)
  (operation nonce-test (displaced 1 0 init 1) n2 (0 1) (enc n1 n2 k))
  (label 6)
  (parent 5)
  (unrealized)
  (shape)
  (maps ((0) ((n1 n1) (n2 n1) (k k))))
  (origs (n1 (0 0))))