cpsa-4.4.4: tst/targetterms2_shapes.tst

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

(comment "CPSA 4.3.1")

(comment "All input read from tst/targetterms2.scm")

(defprotocol targetterms2 basic
  (defrole init
    (vars (a name) (n text))
    (trace (send (enc n (pubk a)))
      (recv (enc n (enc n (enc n (pubk a)) (pubk a)) (pubk a))))
    (non-orig (privk a))
    (uniq-orig n))
  (defrole trans
    (vars (a name) (n text) (m mesg))
    (trace (recv (enc n (pubk a))) (recv m) (send (enc n m (pubk a)))))
  (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 targetterms2
  (vars (n text) (a name))
  (defstrand init 2 (n n) (a a))
  (non-orig (privk a))
  (uniq-orig n)
  (traces
    ((send (enc n (pubk a)))
      (recv (enc n (enc n (enc n (pubk a)) (pubk a)) (pubk a)))))
  (label 0)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton targetterms2
  (vars (n text) (a name))
  (defstrand init 2 (n n) (a a))
  (defstrand trans 3 (m (enc n (enc n (pubk a)) (pubk a))) (n n) (a a))
  (defstrand trans 3 (m (enc n (pubk a))) (n n) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 2) (0 1)) ((2 2) (1 1)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (contracted (m (enc n (pubk a)))) n (1 1)
    (enc n (pubk a)) (enc n (enc n (pubk a)) (pubk a)))
  (traces
    ((send (enc n (pubk a)))
      (recv (enc n (enc n (enc n (pubk a)) (pubk a)) (pubk a))))
    ((recv (enc n (pubk a))) (recv (enc n (enc n (pubk a)) (pubk a)))
      (send (enc n (enc n (enc n (pubk a)) (pubk a)) (pubk a))))
    ((recv (enc n (pubk a))) (recv (enc n (pubk a)))
      (send (enc n (enc n (pubk a)) (pubk a)))))
  (label 7)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (n n))))
  (origs (n (0 0))))

(comment "Nothing left to do")