cpsa-4.4.4: tst/nonaug-prune_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

(comment "CPSA 4.3.1")

(comment "All input read from tst/nonaug-prune.scm")

(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))))
  (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 nonaug-prune
  (vars (n text) (k akey) (A B name))
  (defstrand trans2 2 (n n) (k k) (A B))
  (defstrand trans2 2 (n n) (k k) (A A))
  (defstrand orig 3 (n n) (k k) (A A) (B B))
  (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)
  (unrealized (0 0) (1 0) (2 2))
  (origs (n (2 0)))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton nonaug-prune
  (vars (n text) (k akey) (B name))
  (defstrand trans2 2 (n n) (k k) (A B))
  (defstrand orig 3 (n n) (k k) (A B) (B B))
  (precedes ((0 1) (1 2)) ((1 1) (0 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (displaced 2 1 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 13)
  (parent 0)
  (realized)
  (shape)
  (maps ((0 0 1) ((n n) (A B) (B B) (k k))))
  (origs (n (1 0))))

(defskeleton nonaug-prune
  (vars (n text) (k akey) (B name))
  (defstrand trans2 2 (n n) (k k) (A B))
  (defstrand trans2 2 (n n) (k k) (A B))
  (defstrand orig 3 (n n) (k k) (A B) (B B))
  (precedes ((0 1) (2 2)) ((2 1) (0 0)) ((2 1) (1 0)))
  (non-orig (invk k))
  (uniq-orig n)
  (operation nonce-test (displaced 3 2 orig 2) n (0 0) (enc n B B k))
  (traces ((recv (enc n B k)) (send (enc n B B B k)))
    ((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 14)
  (parent 0)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (A B) (B B) (k k))))
  (origs (n (2 0))))

(defskeleton nonaug-prune
  (vars (n text) (k akey) (A name))
  (defstrand trans2 2 (n n) (k k) (A A))
  (defstrand trans2 2 (n n) (k k) (A A))
  (defstrand orig 3 (n n) (k k) (A A) (B A))
  (defstrand trans2 2 (n n) (k k) (A A))
  (precedes ((2 1) (0 0)) ((2 1) (1 0)) ((2 1) (3 0)) ((3 1) (2 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))
  (traces ((recv (enc n A k)) (send (enc n A A A k)))
    ((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 32)
  (parent 0)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (A A) (B A) (k k))))
  (origs (n (2 0))))

(comment "Nothing left to do")