(herald "Receive priority test protocol")
(comment "CPSA 3.4.0")
(comment "All input read from priority_test.scm")

Trees: 0 3.

Tree 0.

2 1 0 
(defprotocol priority_test basic
  (defrole init
    (vars (n1 n2 n3 n4 text) (k skey))
    (trace (send (enc n1 n1 k)) (recv (enc n1 n2 k))
      (recv (enc n1 n3 k)) (recv (enc n1 n4 k)))
    (non-orig k)
    (uniq-orig n1)
    (priority (2 0) (3 10))))

Item 0, Child: 1.

(enc n1 n4 k) (enc n1 n3 k) (enc n1 n2 k) (enc n1 n1 k) ((n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k)) init priority_test 0
(defskeleton priority_test
  (vars (n1 n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n1)
  (label 0)
  (unrealized (0 1) (0 2) (0 3))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0, Child: 2.

(enc n4 n4 k) (enc n4 n3 k) (enc n4 n2 k) (enc n4 n4 k) ((n1 n4) (n2 n2) (n3 n3) (n4 n4) (k k)) init priority_test 1
(defskeleton priority_test
  (vars (n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n4) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n4)
  (operation encryption-test (displaced 1 0 init 1) (enc n4 n4 k) (0 3))
  (label 1)
  (parent 0)
  (unrealized (0 1) (0 2))
  (origs (n4 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 1.

(enc n2 n2 k) (enc n2 n3 k) (enc n2 n2 k) (enc n2 n2 k) ((n1 n2) (n2 n2) (n3 n3) (n4 n2) (k k)) init priority_test 2
(defskeleton priority_test
  (vars (n2 n3 text) (k skey))
  (defstrand init 4 (n1 n2) (n2 n2) (n3 n3) (n4 n2) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n2)
  (operation encryption-test (displaced 1 0 init 1) (enc n2 n2 k) (0 1))
  (label 2)
  (parent 1)
  (unrealized (0 2))
  (origs (n2 (0 0))))

Tree 3.

5 4 3 
(defprotocol priority_test basic
  (defrole init
    (vars (n1 n2 n3 n4 text) (k skey))
    (trace (send (enc n1 n1 k)) (recv (enc n1 n2 k))
      (recv (enc n1 n3 k)) (recv (enc n1 n4 k)))
    (non-orig k)
    (uniq-orig n1)
    (priority (2 0) (3 10))))

Item 3, Child: 4.

(enc n1 n4 k) (enc n1 n3 k) (enc n1 n2 k) (enc n1 n1 k) ((n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k)) init priority_test 3
(defskeleton priority_test
  (vars (n1 n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n1)
  (label 3)
  (unrealized (0 1) (0 2) (0 3))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 4, Parent: 3, Child: 5.

(enc n3 n4 k) (enc n3 n3 k) (enc n3 n2 k) (enc n3 n3 k) ((n1 n3) (n2 n2) (n3 n3) (n4 n4) (k k)) init priority_test 4
(defskeleton priority_test
  (vars (n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n3) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n3)
  (operation encryption-test (displaced 1 0 init 1) (enc n3 n3 k) (0 2))
  (label 4)
  (parent 3)
  (unrealized (0 1) (0 3))
  (origs (n3 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 5, Parent: 4.

(enc n2 n4 k) (enc n2 n2 k) (enc n2 n2 k) (enc n2 n2 k) ((n1 n2) (n2 n2) (n3 n2) (n4 n4) (k k)) init priority_test 5
(defskeleton priority_test
  (vars (n2 n4 text) (k skey))
  (defstrand init 4 (n1 n2) (n2 n2) (n3 n2) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n2)
  (operation encryption-test (displaced 1 0 init 1) (enc n2 n2 k) (0 1))
  (label 5)
  (parent 4)
  (unrealized (0 3))
  (origs (n2 (0 0))))