cpsa-2.2.2: tst/deorig_simple.tst

(comment "CPSA 2.2.2")
(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))

(comment "Nothing left to do")