cpsa-4.4.4: tst/fragile_pruning_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(comment "CPSA 4.3.1")
(comment "All input read from tst/fragile_pruning.scm")
(defprotocol fragile_pruning basic
(defrole init
(vars (k akey) (n n1 n2 n3 text))
(trace (send (enc n k)) (recv (enc n n1 k)) (recv (enc n n2 k))
(recv (enc n n3 k)) (send (enc n n1 n2 n3 k))
(recv (enc n n1 n2 n3 n k)))
(non-orig (invk k))
(uniq-orig n))
(defrole adder
(vars (k akey) (n new text))
(trace (recv (enc n k)) (send (enc n new k)))
(uniq-orig new))
(defrole final
(vars (k akey) (n n1 n2 n3 text))
(trace (recv (enc n n1 n2 n3 k)) (send (enc n n1 n2 n3 n k))))
(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 fragile_pruning
(vars (n n1 n2 n3 text) (k akey))
(defstrand init 6 (n n) (n1 n1) (n2 n2) (n3 n3) (k k))
(non-orig (invk k))
(uniq-orig n n1 n2 n3)
(traces
((send (enc n k)) (recv (enc n n1 k)) (recv (enc n n2 k))
(recv (enc n n3 k)) (send (enc n n1 n2 n3 k))
(recv (enc n n1 n2 n3 n k))))
(label 0)
(unrealized (0 1) (0 2) (0 3) (0 5))
(origs (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton fragile_pruning
(vars (n new text) (k akey))
(defstrand init 6 (n n) (n1 new) (n2 new) (n3 new) (k k))
(defstrand adder 2 (n n) (new new) (k k))
(defstrand final 2 (n n) (n1 new) (n2 new) (n3 new) (k k))
(precedes ((0 0) (1 0)) ((0 4) (2 0)) ((1 1) (0 1)) ((2 1) (0 5)))
(non-orig (invk k))
(uniq-orig n new)
(operation nonce-test (displaced 3 0 init 5) n (2 0) (enc n k)
(enc n new k))
(traces
((send (enc n k)) (recv (enc n new k)) (recv (enc n new k))
(recv (enc n new k)) (send (enc n new new new k))
(recv (enc n new new new n k)))
((recv (enc n k)) (send (enc n new k)))
((recv (enc n new new new k)) (send (enc n new new new n k))))
(label 20)
(parent 0)
(realized)
(shape)
(maps ((0) ((k k) (n n) (n1 new) (n2 new) (n3 new))))
(origs (n (0 0)) (new (1 1))))
(defskeleton fragile_pruning
(vars (n new new-0 text) (k akey))
(defstrand init 6 (n n) (n1 new) (n2 new) (n3 new-0) (k k))
(defstrand adder 2 (n n) (new new) (k k))
(defstrand adder 2 (n n) (new new-0) (k k))
(defstrand final 2 (n n) (n1 new) (n2 new) (n3 new-0) (k k))
(precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 4) (3 0)) ((1 1) (0 1))
((2 1) (0 3)) ((3 1) (0 5)))
(non-orig (invk k))
(uniq-orig n new new-0)
(operation nonce-test (displaced 4 0 init 5) n (3 0) (enc n k)
(enc n new k) (enc n new-0 k))
(traces
((send (enc n k)) (recv (enc n new k)) (recv (enc n new k))
(recv (enc n new-0 k)) (send (enc n new new new-0 k))
(recv (enc n new new new-0 n k)))
((recv (enc n k)) (send (enc n new k)))
((recv (enc n k)) (send (enc n new-0 k)))
((recv (enc n new new new-0 k)) (send (enc n new new new-0 n k))))
(label 47)
(parent 0)
(realized)
(shape)
(maps ((0) ((k k) (n n) (n1 new) (n2 new) (n3 new-0))))
(origs (n (0 0)) (new-0 (2 1)) (new (1 1))))
(defskeleton fragile_pruning
(vars (n new new-0 text) (k akey))
(defstrand init 6 (n n) (n1 new) (n2 new-0) (n3 new) (k k))
(defstrand adder 2 (n n) (new new) (k k))
(defstrand adder 2 (n n) (new new-0) (k k))
(defstrand final 2 (n n) (n1 new) (n2 new-0) (n3 new) (k k))
(precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 4) (3 0)) ((1 1) (0 1))
((2 1) (0 2)) ((3 1) (0 5)))
(non-orig (invk k))
(uniq-orig n new new-0)
(operation nonce-test (displaced 4 0 init 5) n (3 0) (enc n k)
(enc n new k) (enc n new-0 k))
(traces
((send (enc n k)) (recv (enc n new k)) (recv (enc n new-0 k))
(recv (enc n new k)) (send (enc n new new-0 new k))
(recv (enc n new new-0 new n k)))
((recv (enc n k)) (send (enc n new k)))
((recv (enc n k)) (send (enc n new-0 k)))
((recv (enc n new new-0 new k)) (send (enc n new new-0 new n k))))
(label 62)
(parent 0)
(realized)
(shape)
(maps ((0) ((k k) (n n) (n1 new) (n2 new-0) (n3 new))))
(origs (n (0 0)) (new-0 (2 1)) (new (1 1))))
(defskeleton fragile_pruning
(vars (n new new-0 text) (k akey))
(defstrand init 6 (n n) (n1 new) (n2 new-0) (n3 new-0) (k k))
(defstrand adder 2 (n n) (new new) (k k))
(defstrand adder 2 (n n) (new new-0) (k k))
(defstrand final 2 (n n) (n1 new) (n2 new-0) (n3 new-0) (k k))
(precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 4) (3 0)) ((1 1) (0 1))
((2 1) (0 2)) ((3 1) (0 5)))
(non-orig (invk k))
(uniq-orig n new new-0)
(operation nonce-test (displaced 4 0 init 5) n (3 0) (enc n k)
(enc n new k) (enc n new-0 k))
(traces
((send (enc n k)) (recv (enc n new k)) (recv (enc n new-0 k))
(recv (enc n new-0 k)) (send (enc n new new-0 new-0 k))
(recv (enc n new new-0 new-0 n k)))
((recv (enc n k)) (send (enc n new k)))
((recv (enc n k)) (send (enc n new-0 k)))
((recv (enc n new new-0 new-0 k))
(send (enc n new new-0 new-0 n k))))
(label 65)
(parent 0)
(realized)
(shape)
(maps ((0) ((k k) (n n) (n1 new) (n2 new-0) (n3 new-0))))
(origs (n (0 0)) (new-0 (2 1)) (new (1 1))))
(defskeleton fragile_pruning
(vars (n new new-0 new-1 text) (k akey))
(defstrand init 6 (n n) (n1 new) (n2 new-0) (n3 new-1) (k k))
(defstrand adder 2 (n n) (new new) (k k))
(defstrand adder 2 (n n) (new new-0) (k k))
(defstrand adder 2 (n n) (new new-1) (k k))
(defstrand final 2 (n n) (n1 new) (n2 new-0) (n3 new-1) (k k))
(precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((0 4) (4 0))
((1 1) (0 1)) ((2 1) (0 2)) ((3 1) (0 3)) ((4 1) (0 5)))
(non-orig (invk k))
(uniq-orig n new new-0 new-1)
(operation nonce-test (displaced 5 0 init 5) n (4 0) (enc n k)
(enc n new k) (enc n new-0 k) (enc n new-1 k))
(traces
((send (enc n k)) (recv (enc n new k)) (recv (enc n new-0 k))
(recv (enc n new-1 k)) (send (enc n new new-0 new-1 k))
(recv (enc n new new-0 new-1 n k)))
((recv (enc n k)) (send (enc n new k)))
((recv (enc n k)) (send (enc n new-0 k)))
((recv (enc n k)) (send (enc n new-1 k)))
((recv (enc n new new-0 new-1 k))
(send (enc n new new-0 new-1 n k))))
(label 111)
(parent 0)
(realized)
(shape)
(maps ((0) ((k k) (n n) (n1 new) (n2 new-0) (n3 new-1))))
(origs (n (0 0)) (new-1 (3 1)) (new-0 (2 1)) (new (1 1))))
(comment "Nothing left to do")