cpsa-2.2.2: tst/nonaug-prune.tst

(comment "CPSA 2.2.2")
(comment "All input read")

(defprotocol nonaug-prune basic
  (defrole orig
    (vars (n text) (A B name) (k akey))
    (trace (send (enc n B B k)) (send (enc n A k))
      (recv (enc n A A A k)))
    (non-orig (invk k))
    (uniq-orig n))
  (defrole trans1
    (vars (n text) (A C name) (k akey))
    (trace (recv (enc n A A k)) (recv (enc n A k))
      (send (enc n n C k))))
  (defrole trans2
    (vars (n text) (A name) (k akey))
    (trace (recv (enc n A k)) (send (enc n A A A k)))))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (precedes ((2 0) (0 0)) ((2 0) (1 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n A k)) (send (enc n A A A k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k))))
  (label 0)
  (seen 2)
  (unrealized (0 0) (1 0) (2 2))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans1 3) n (2 2) (enc n B k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 1)
  (parent 0)
  (seen 4)
  (unrealized (0 0) (1 2) (2 1))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans2 2) n (2 2) (enc n A k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 2)
  (parent 0)
  (seen 5)
  (unrealized (0 0) (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (precedes ((0 1) (1 2)) ((1 0) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (displaced 3 0 trans2 2) n (2 2) (enc n A k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))))
  (label 3)
  (parent 0)
  (seen 6)
  (unrealized (0 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 1) (2 1)) ((2 2) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (2 1) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 4)
  (parent 1)
  (seen 7)
  (unrealized (0 0) (1 2))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 0) (0 0)) ((1 1) (2 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (2 0) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 5)
  (parent 2)
  (seen 8)
  (unrealized (0 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (precedes ((0 1) (1 2)) ((1 1) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (0 0) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))))
  (label 6)
  (parent 3)
  (unrealized)
  (shape))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 1) (1 1)) ((1 2) (0 2))
    ((2 1) (0 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans2 2) n (1 2) (enc n B k)
    (enc n n C k) (enc n B B k))
  (traces
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))
    ((recv (enc n B k)) (send (enc n B B B k))))
  (label 7)
  (parent 4)
  (seen 9)
  (unrealized (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 1) (0 0)) ((1 1) (2 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (0 0) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 8)
  (parent 5)
  (seen 6)
  (unrealized (0 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (precedes ((0 0) (1 0)) ((0 1) (1 1)) ((0 1) (2 0)) ((1 2) (0 2))
    ((2 1) (0 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (2 0) (enc n B B k))
  (traces
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))
    ((recv (enc n B k)) (send (enc n B B B k))))
  (label 9)
  (parent 7)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (3 0)) ((1 1) (0 0)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans1 3) n (0 0) (enc n B k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 10)
  (parent 8)
  (seen 13)
  (unrealized (3 1))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 0) (3 0)) ((1 1) (0 0)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 1) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans2 2) n (0 0) (enc n A k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 11)
  (parent 8)
  (seen 14)
  (unrealized (0 0) (3 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 1) (2 0)) ((2 1) (0 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (displaced 3 2 trans2 2) n (0 0) (enc n A k)
    (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 12)
  (parent 8)
  (unrealized (0 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (3 0)) ((1 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 2))
    ((3 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (3 1) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 13)
  (parent 10)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A A) (B B) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 2)) ((3 1) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (3 0) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 14)
  (parent 11)
  (unrealized (0 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A name) (k akey))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand orig 3 (n n) (A A) (B A) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 1) (2 0)) ((2 1) (0 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (contracted (B A)) n (0 0) (enc n A k)
    (enc n A A k) (enc n A A A k))
  (traces ((recv (enc n A k)) (send (enc n A A A k)))
    ((send (enc n A A k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 15)
  (parent 12)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 0)) ((2 1) (1 2))
    ((3 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans1 3) n (0 0) (enc n B k)
    (enc n B B k) (enc n B B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 16)
  (parent 12)
  (seen 20)
  (unrealized (3 1))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (precedes ((1 1) (0 0)) ((1 1) (2 0)) ((2 1) (1 2)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation generalization deleted (3 0))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k))))
  (label 17)
  (parent 13)
  (seen 6)
  (unrealized)
  (shape)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (A name) (k akey))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand orig 3 (n n) (A A) (B A) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (defstrand trans2 2 (n n) (A A) (k k))
  (precedes ((1 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 2)) ((3 1) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (contracted (B A)) n (0 0) (enc n A k)
    (enc n A A k) (enc n A A A k))
  (traces ((recv (enc n A k)) (send (enc n A A A k)))
    ((send (enc n A A k)) (send (enc n A k)) (recv (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k)))
    ((recv (enc n A k)) (send (enc n A A A k))))
  (label 18)
  (parent 14)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (4 0)) ((1 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 2))
    ((3 1) (0 0)) ((4 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand trans1 3) n (0 0) (enc n B k)
    (enc n B B k) (enc n B B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 19)
  (parent 14)
  (seen 21)
  (unrealized (4 1))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (3 0)) ((1 1) (2 0)) ((1 1) (3 1)) ((2 1) (0 0))
    ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (3 1) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 20)
  (parent 16)
  (seen 15)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (B C name) (k akey))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand orig 3 (n n) (A B) (B B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans2 2 (n n) (A B) (k k))
  (defstrand trans1 3 (n n) (A B) (C C) (k k))
  (precedes ((1 0) (4 0)) ((1 1) (2 0)) ((1 1) (3 0)) ((1 1) (4 1))
    ((2 1) (1 2)) ((3 1) (0 0)) ((4 2) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (added-strand orig 2) n (4 1) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B k)) (send (enc n B B B k)))
    ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))))
  (label 21)
  (parent 19)
  (seen 13)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")