cpsa-4.4.4: tst/wonthull2_shapes.tst

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

(herald wonthull2 (bound 9))

(comment "CPSA 4.3.1")

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

(comment "Strand count bounded at 9")

(defprotocol wonthull2 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (cat (enc x1 x3 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    (non-orig (privk a))
    (uniq-orig x3))
  (defrole resp
    (vars (a name) (y1 y2 y3 text))
    (trace (recv (enc y1 y2 (pubk a)))
      (send (enc "okay" y3 y1 (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 wonthull2
  (vars (x1 x2 x3 x4 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (non-orig (privk a))
  (uniq-orig x3)
  (traces
    ((send (cat (enc x1 x3 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a)))))
  (label 0)
  (unrealized (0 1))
  (origs (x3 (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x2 y3 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x2) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x3 y3) (x4 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 x2 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (pubk a)) (enc y3 x2 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x2 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 3)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))
  (origs (y3 (0 0))))

(defskeleton wonthull2
  (vars (x2 y3 y3-0 text) (a name))
  (defstrand init 2 (x1 y3) (x2 x2) (x3 y3-0) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3-0) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3-0)
  (operation generalization forgot y3)
  (traces
    ((send (cat (enc y3 y3-0 (pubk a)) (enc y3-0 x2 (pubk a))))
      (recv (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 y3-0 (pubk a)))
      (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 19)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (x1 y3) (x2 x2) (x3 y3-0) (x4 y3))))
  (origs (y3-0 (0 0))))

(comment "Nothing left to do")

(defprotocol wonthull2 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (cat (enc x1 x3 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    (non-orig (privk a))
    (uniq-orig x3))
  (defrole resp
    (vars (a name) (y1 y2 y3 text))
    (trace (recv (enc y1 y2 (pubk a)))
      (send (enc "okay" y3 y1 (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 wonthull2
  (vars (x1 x3 x1-0 x3-0 text) (a a-0 name))
  (defstrand init 2 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (traces
    ((send (cat (enc x1-0 x3-0 (pubk a)) (enc x3-0 x3 (pubk a))))
      (recv (enc "okay" x3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0)))
      (send (enc "okay" x3 x1 (pubk a-0)))))
  (label 20)
  (unrealized (0 1))
  (origs (x3-0 (0 0)))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton wonthull2
  (vars (x3 x1 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 2 1 resp 2) x1-0 (0 1)
    (enc "okay" x3 x1-0 (pubk a)) (enc x1-0 x3 (pubk a))
    (enc x1 x1-0 (pubk a)))
  (traces
    ((send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 25)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))
  (origs (x3 (0 0))))

(defskeleton wonthull2
  (vars (x3 x1 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a)))))
  (label 28)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))
  (origs (x3 (0 0))))

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 3 2 resp 2) x1-0 (0 1)
    (enc "okay" x3 x1-0 (pubk a)) (enc "okay" y3 x1-0 (pubk a))
    (enc x1-0 x3 (pubk a)) (enc x1 x1-0 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 43)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a))))
  (origs (y3 (0 0))))

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (x1 y3) (x2 x3) (x3 y3-0) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 y3-0) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3-0)
  (operation generalization forgot (privk a-0))
  (traces
    ((send (cat (enc y3 y3-0 (pubk a)) (enc y3-0 x3 (pubk a))))
      (recv (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 y3-0 (pubk a)))
      (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 229)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 y3) (x3-0 y3-0) (a-0 a-0))))
  (origs (y3-0 (0 0))))

(comment "Nothing left to do")