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

(defprotocol deorig-simple basic
  (defrole init
    (vars (k akey) (x2 text))
    (trace (send (enc x2 k)) (recv x2))
    (non-orig (invk k))
    (uniq-orig x2))
  (defrole resp
    (vars (k akey) (y2 y3 text))
    (trace (recv (enc y2 k)) (send y3))))

(defskeleton deorig-simple
  (vars (x2 text) (k akey))
  (defstrand init 2 (x2 x2) (k k))
  (non-orig (invk k))
  (uniq-orig x2)
  (traces ((send (enc x2 k)) (recv x2)))
  (label 0)
  (unrealized (0 1))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol deorig-simple basic
  (defrole init
    (vars (k akey) (x2 text))
    (trace (send (enc x2 k)) (recv x2))
    (non-orig (invk k))
    (uniq-orig x2))
  (defrole resp
    (vars (k akey) (y2 y3 text))
    (trace (recv (enc y2 k)) (send y3))))

(defskeleton deorig-simple
  (vars (x2 text) (k akey))
  (defstrand init 2 (x2 x2) (k k))
  (defstrand resp 2 (y2 x2) (y3 x2) (k k))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk k))
  (uniq-orig x2)
  (traces ((send (enc x2 k)) (recv x2)) ((recv (enc x2 k)) (send x2)))
  (label 1)
  (unrealized)
  (shape)
  (maps ((0 1) ((k k) (x2 x2)))))

(comment "Nothing left to do")