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

Trees: 0 2 3 5.

Tree 0.

1 0 
(defprotocol lttest 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 lttest 0 
(defskeleton lttest
  (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 lttest 1 (realized)
(defskeleton lttest
  (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 lttest 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 lttest 2 
(defskeleton lttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (lt (n1 n2))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 2)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "empty cohort"))

Tree 3.

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

Item 3, Child: 4.

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

Item 4, Parent: 3.

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

Tree 5.

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

Item 5.

n2 (cat n1 (enc n1 n2 k)) n ((n1 n1) (n2 n2) (n n) (k k)) init lttest2 5 
(defskeleton lttest2
  (vars (n n1 n2 text) (k skey))
  (defstrand init 3 (n1 n1) (n2 n2) (n n) (k k))
  (lt (n n1) (n2 n))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 5)
  (unrealized (0 2))
  (origs (n1 (0 1)) (n2 (0 1)))
  (comment "empty cohort"))