cpsa-2.2.0: tst/deorig_simple.scm

;;;  Deorig_simple:     Demonstrates the same incompleteness as
;;;                     deorig_contract, but with fewer messages.
;;;
;;;  This simply sets up the archetypal nonce test for an init strand
;;;  but the resp role is only a partial match for the test.  In particular,
;;;  it sends a different value than it receives.  The obvious shape is one
;;;  in which the resp strand sends the same value it receives, but this
;;;  shape is not found.

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

(defskeleton deorig-simple
   (vars)
   (defstrand init 2)
)

(defskeleton deorig-simple
   (vars (k akey) (x2 text))
   (defstrand init 2 (k k) (x2 x2))
   (defstrand resp 2 (k k) (y2 x2) (y3 x2))
   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
)