cpsa-4.4.9: tst/dev-subatomic-open-closed.tst

(herald dev-subatomic-open-closed
  (comment "Version that uses (dev const) pairs for locations"))

(comment "CPSA 4.4.9")
(comment "All input read from tst/dev-subatomic-open-closed.scm")

(defprotocol subatomic-open-closed basic
  (defrole dev-up
    (vars (k skey) (d dev) (o name) (start-ch chan))
    (trace (recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send (enc "up" k)))
    (auth start-ch))
  (defrole owner-power-dev
    (vars (k skey) (o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "open" d o n k)) (recv n)))
  (defrole owner-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "close" d o n k)) (recv n)))
  (defrole dev-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "open" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o o)) (send n))
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole dev-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "close" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send n))
    (gen-st (cat "st-k" o k)))
  (defrole dev-pass
    (vars (k skey) (n text) (d dev) (o name))
    (trace (load (cat d "lk") (cat "st-k" o k))
      (load (cat d "ls") (cat "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    (uniq-orig n)
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole user-pass
    (vars (k skey))
    (trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z2 (idx 2)) (p "dev-up" z1 (idx 2))
          (p "dev-up" "k" z2 k) (p "dev-up" "k" z1 k))
        (= z1 z2))))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1)
          (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule discreteBefore
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 2)) (trans z (idx 1)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-close-at-2
    (forall ((z strd))
      (implies (p "dev-close" z (idx 3)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-up" z (idx 2)) (prec z (idx 1) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 3)) (prec z (idx 2) z1 i))))))
  (defgenrule cau-dev-pass-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule eff-dev-pass-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "dev-pass" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule gen-st-dev-open-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-open" z (idx 1)) (p "dev-open" "o" z o))
        (gen-st (cat "st" o o)))))
  (defgenrule gen-st-dev-close-0
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-close" z (idx 1)) (p "dev-close" "k" z k)
          (p "dev-close" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-pass" z (idx 1)) (p "dev-pass" "o" z o))
        (gen-st (cat "st" o o))))))

(defskeleton subatomic-open-closed
  (vars (k skey) (o name) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (deflistener k)
  (uniq-orig k)
  (conf start-ch)
  (facts (no-state-split))
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((recv k) (send k)))
  (label 0)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch))))
  (origs (k (0 0)))
  (comment "Not a skeleton"))

(defskeleton subatomic-open-closed
  (vars (k skey) (o name) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (deflistener k)
  (precedes ((0 0) (1 0)))
  (uniq-orig k)
  (conf start-ch)
  (facts (no-state-split))
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((recv k) (send k)))
  (label 1)
  (parent 0)
  (unrealized (0 1) (1 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch))))
  (origs (k (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (o name) (pt pt-0 pval) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (deflistener k)
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((0 0) (2 0)) ((2 2) (1 0)))
  (uniq-orig k)
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (rule eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation nonce-test (added-strand dev-up 2) k (1 0)
    (ch-msg start-ch (cat "power-up" o k)))
  (strand-map 0 1)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((recv k) (send k))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt "st-k" o k))
      (stor (cat d "ls") (cat pt-0 "st" o))))
  (label 2)
  (parent 1)
  (unrealized (0 1) (1 0))
  (dead)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch))))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol subatomic-open-closed basic
  (defrole dev-up
    (vars (k skey) (d dev) (o name) (start-ch chan))
    (trace (recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send (enc "up" k)))
    (auth start-ch))
  (defrole owner-power-dev
    (vars (k skey) (o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "open" d o n k)) (recv n)))
  (defrole owner-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "close" d o n k)) (recv n)))
  (defrole dev-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "open" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o o)) (send n))
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole dev-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "close" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send n))
    (gen-st (cat "st-k" o k)))
  (defrole dev-pass
    (vars (k skey) (n text) (d dev) (o name))
    (trace (load (cat d "lk") (cat "st-k" o k))
      (load (cat d "ls") (cat "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    (uniq-orig n)
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole user-pass
    (vars (k skey))
    (trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z2 (idx 2)) (p "dev-up" z1 (idx 2))
          (p "dev-up" "k" z2 k) (p "dev-up" "k" z1 k))
        (= z1 z2))))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1)
          (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule discreteBefore
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 2)) (trans z (idx 1)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-close-at-2
    (forall ((z strd))
      (implies (p "dev-close" z (idx 3)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-up" z (idx 2)) (prec z (idx 1) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 3)) (prec z (idx 2) z1 i))))))
  (defgenrule cau-dev-pass-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule eff-dev-pass-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "dev-pass" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule gen-st-dev-open-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-open" z (idx 1)) (p "dev-open" "o" z o))
        (gen-st (cat "st" o o)))))
  (defgenrule gen-st-dev-close-0
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-close" z (idx 1)) (p "dev-close" "k" z k)
          (p "dev-close" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-pass" z (idx 1)) (p "dev-pass" "o" z o))
        (gen-st (cat "st" o o))))))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pval))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (uniq-orig n)
  (facts (no-state-split) (useLocName))
  (traces
    ((load (cat d "lk") (cat pt "st-k" o k))
      (load (cat d "ls") (cat pt-0 "st" o o))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 3)
  (realized)
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (n (0 3)))
  (comment "Not closed under rules"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pval))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (facts (no-state-split) (useLocName))
  (rule gen-st-dev-pass-0 gen-st-dev-pass-1)
  (traces
    ((load (cat d "lk") (cat pt "st-k" o k))
      (load (cat d "ls") (cat pt-0 "st" o o))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 4)
  (parent 3)
  (unrealized (0 0) (0 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (n (0 3)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((1 2) (0 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (auth start-ch)
  (facts (no-state-split) (useLocName))
  (leads-to ((1 1) (0 0)))
  (rule eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o k)) (0 0))
  (strand-map 0)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 5)
  (parent 4)
  (unrealized (0 1) (1 0))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (precedes ((1 2) (0 0)) ((2 0) (1 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split) (useLocName))
  (leads-to ((1 1) (0 0)))
  (operation channel-test (added-strand owner-power-dev 1)
    (ch-msg start-ch (cat "power-up" o k)) (1 0))
  (strand-map 0 1)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send start-ch (cat "power-up" o k))))
  (label 6)
  (parent 5)
  (unrealized (0 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k k-0 skey) (n n-0 text) (o name)
    (pt pt-0 pt-1 pt-2 pval) (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (defstrand dev-open 3 (d d) (k k-0) (n n-0) (o o))
  (precedes ((1 2) (3 1)) ((2 0) (1 0)) ((3 2) (0 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k) (cat "st-k" o k-0))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split) (useLocName))
  (leads-to ((1 1) (0 0)) ((3 2) (0 1)))
  (rule cau-dev-pass-1 discreteBefore gen-st-dev-open-1
    trRl_dev-open-at-2)
  (operation channel-test (added-strand dev-open 3)
    (ch-msg (cat d "ls") (cat pt "st" o o)) (0 1))
  (strand-map 0 1 2)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send start-ch (cat "power-up" o k)))
    ((recv (enc "open" d o n-0 k-0))
      (load (cat d "lk") (cat pt-2 "st-k" o k-0))
      (stor (cat d "ls") (cat pt "st" o o))))
  (label 7)
  (parent 6)
  (unrealized (3 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((1 0) (3 0)) ((2 2) (0 0)) ((3 2) (2 1)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split) (useLocName))
  (leads-to ((2 2) (0 1)) ((3 1) (0 0)) ((3 1) (2 1)))
  (rule discreteBefore eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o k)) (3 1))
  (strand-map 0 2 3 1)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((send start-ch (cat "power-up" o k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 8)
  (parent 7)
  (realized)
  (shape)
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (pt-0 (3 1)) (pt-1 (3 2)) (pt (2 2)) (n (0 3))))

(comment "Nothing left to do")

(defprotocol subatomic-open-closed basic
  (defrole dev-up
    (vars (k skey) (d dev) (o name) (start-ch chan))
    (trace (recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send (enc "up" k)))
    (auth start-ch))
  (defrole owner-power-dev
    (vars (k skey) (o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "open" d o n k)) (recv n)))
  (defrole owner-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "close" d o n k)) (recv n)))
  (defrole dev-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "open" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o o)) (send n))
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole dev-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "close" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send n))
    (gen-st (cat "st-k" o k)))
  (defrole dev-pass
    (vars (k skey) (n text) (d dev) (o name))
    (trace (load (cat d "lk") (cat "st-k" o k))
      (load (cat d "ls") (cat "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    (uniq-orig n)
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole user-pass
    (vars (k skey))
    (trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z2 (idx 2)) (p "dev-up" z1 (idx 2))
          (p "dev-up" "k" z2 k) (p "dev-up" "k" z1 k))
        (= z1 z2))))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1)
          (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule discreteBefore
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 2)) (trans z (idx 1)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-close-at-2
    (forall ((z strd))
      (implies (p "dev-close" z (idx 3)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-up" z (idx 2)) (prec z (idx 1) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 3)) (prec z (idx 2) z1 i))))))
  (defgenrule cau-dev-pass-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule eff-dev-pass-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "dev-pass" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule gen-st-dev-open-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-open" z (idx 1)) (p "dev-open" "o" z o))
        (gen-st (cat "st" o o)))))
  (defgenrule gen-st-dev-close-0
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-close" z (idx 1)) (p "dev-close" "k" z k)
          (p "dev-close" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-pass" z (idx 1)) (p "dev-pass" "o" z o))
        (gen-st (cat "st" o o))))))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o o-0 name) (pt pt-0 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o-0))
  (uniq-orig k n)
  (conf start-ch)
  (facts (no-state-split))
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt "st-k" o-0 k))
      (load (cat d "ls") (cat pt-0 "st" o-0 o-0))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 9)
  (unrealized (0 1) (1 0) (1 2))
  (preskeleton)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o-0))))
  (origs (n (1 3)) (k (0 0)))
  (comment "Not a skeleton"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o o-0 name) (pt pt-0 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o-0))
  (precedes ((0 0) (1 0)))
  (uniq-orig k n)
  (conf start-ch)
  (facts (no-state-split))
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt "st-k" o-0 k))
      (load (cat d "ls") (cat pt-0 "st" o-0 o-0))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 10)
  (parent 9)
  (unrealized (0 1) (1 0) (1 2))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o-0))))
  (origs (n (1 3)) (k (0 0)))
  (comment "Not closed under rules"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o o-0 name) (pt pt-0 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o-0))
  (precedes ((0 0) (1 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o-0 o-0) (cat "st-k" o-0 k))
  (conf start-ch)
  (facts (no-state-split))
  (rule gen-st-dev-pass-0 gen-st-dev-pass-1)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt "st-k" o-0 k))
      (load (cat d "ls") (cat pt-0 "st" o-0 o-0))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 11)
  (parent 10)
  (unrealized (0 1) (1 0) (1 1) (1 2))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o-0))))
  (origs (n (1 3)) (k (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o o-0 name) (pt pt-0 pt-1 pval)
    (start-ch start-ch-0 chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o-0))
  (defstrand dev-up 3 (d d) (k k) (o o-0) (start-ch start-ch-0))
  (precedes ((0 0) (2 0)) ((2 2) (1 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o-0 o-0) (cat "st-k" o-0 k))
  (conf start-ch)
  (auth start-ch-0)
  (facts (no-state-split))
  (leads-to ((2 1) (1 0)))
  (rule eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o-0 k)) (1 0))
  (strand-map 0 1)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o-0 k))
      (load (cat d "ls") (cat pt "st" o-0 o-0))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k)))
    ((recv start-ch-0 (cat "power-up" o-0 k))
      (stor (cat d "lk") (cat pt-0 "st-k" o-0 k))
      (stor (cat d "ls") (cat pt-1 "st" o-0))))
  (label 12)
  (parent 11)
  (unrealized (0 1) (1 1) (1 2) (2 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o-0))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((0 0) (2 0)) ((2 2) (1 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 1) (1 0)))
  (operation channel-test (displaced 3 0 owner-power-dev 1)
    (ch-msg start-ch-0 (cat "power-up" o-0 k)) (2 0))
  (strand-map 0 1 2)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 13)
  (parent 12)
  (unrealized (0 1) (1 1) (1 2))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k k-0 skey) (n n-0 text) (o name)
    (pt pt-0 pt-1 pt-2 pval) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand dev-open 3 (d d) (k k-0) (n n-0) (o o))
  (precedes ((0 0) (2 0)) ((2 2) (3 1)) ((3 2) (1 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k) (cat "st-k" o k-0))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 1) (1 0)) ((3 2) (1 1)))
  (rule cau-dev-pass-1 discreteBefore gen-st-dev-open-1
    trRl_dev-open-at-2)
  (operation channel-test (added-strand dev-open 3)
    (ch-msg (cat d "ls") (cat pt "st" o o)) (1 1))
  (strand-map 0 1 2)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((recv (enc "open" d o n-0 k-0))
      (load (cat d "lk") (cat pt-2 "st-k" o k-0))
      (stor (cat d "ls") (cat pt "st" o o))))
  (label 14)
  (parent 13)
  (unrealized (0 1) (1 2) (3 1))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (2 1)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (rule discreteBefore eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o k)) (3 1))
  (strand-map 0 1 3 2)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 15)
  (parent 14)
  (unrealized (0 1) (1 2) (2 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (2 1)) ((4 0) (2 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (operation encryption-test (added-strand owner-open 1)
    (enc "open" d o n-0 k) (2 0))
  (strand-map 0 1 2 3)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))))
  (label 16)
  (parent 15)
  (unrealized (0 1) (1 2))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((2 2) (1 0)) ((3 2) (2 1))
    ((4 1) (2 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (operation encryption-test (added-listener k) (enc "open" d o n-0 k)
    (2 0))
  (strand-map 0 1 2 3)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))) ((recv k) (send k)))
  (label 17)
  (parent 15)
  (unrealized (0 1) (4 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (defstrand user-pass 1 (k k))
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (2 1)) ((4 0) (2 0))
    ((5 0) (1 2)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (operation encryption-test (added-strand user-pass 1)
    (enc "may I pass" k) (1 2))
  (strand-map 0 1 2 3 4)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))) ((send (enc "may I pass" k))))
  (label 18)
  (parent 16)
  (unrealized (0 1))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((2 2) (1 0)) ((3 2) (2 1))
    ((4 0) (2 0)) ((5 1) (1 2)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (operation encryption-test (added-listener k) (enc "may I pass" k)
    (1 2))
  (strand-map 0 1 2 3 4)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))) ((recv k) (send k)))
  (label 19)
  (parent 16)
  (unrealized (0 1) (5 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (4 0)) ((4 1) (2 0)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (rule eff-dev-up-1 power-deliver-once trRl_dev-up-at-1)
  (operation nonce-test (added-strand dev-up 2) k (4 0)
    (ch-msg start-ch (cat "power-up" o k)))
  (strand-map 0 1 2 3 4)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))) ((recv k) (send k)))
  (label 20)
  (parent 17)
  (unrealized (0 1) (4 0))
  (dead)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "empty cohort"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (defstrand user-pass 1 (k k))
  (defstrand dev-up 4 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((0 0) (5 0)) ((2 2) (1 0)) ((3 0) (2 0)) ((4 0) (1 2))
    ((5 2) (2 1)) ((5 3) (0 1)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((5 1) (1 0)) ((5 1) (2 1)))
  (rule power-deliver-once trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation encryption-test (added-strand dev-up 4) (enc "up" k) (0 1))
  (strand-map 0 1 2 4 5 3)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((send (enc "open" d o n-0 k))) ((send (enc "may I pass" k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)) (send (enc "up" k))))
  (label 21)
  (parent 18)
  (realized)
  (shape)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (origs (pt-0 (5 1)) (pt-1 (5 2)) (pt (2 2)) (n (1 3)) (k (0 0))))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (defstrand user-pass 1 (k k))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((0 0) (6 0)) ((2 2) (1 0)) ((3 2) (2 1))
    ((4 0) (2 0)) ((5 0) (1 2)) ((6 1) (0 1)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (operation encryption-test (added-listener k) (enc "up" k) (0 1))
  (strand-map 0 1 2 3 4 5)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))) ((send (enc "may I pass" k)))
    ((recv k) (send k)))
  (label 22)
  (parent 18)
  (unrealized (6 0))
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (2 1)) ((3 2) (5 0))
    ((4 0) (2 0)) ((5 1) (1 2)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (rule eff-dev-up-1 power-deliver-once trRl_dev-up-at-1)
  (operation nonce-test (added-strand dev-up 2) k (5 0)
    (ch-msg start-ch (cat "power-up" o k)))
  (strand-map 0 1 2 3 4 5)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))) ((recv k) (send k)))
  (label 23)
  (parent 19)
  (unrealized (0 1) (5 0))
  (dead)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "empty cohort"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-open 1 (d d) (k k) (n n-0) (o o))
  (defstrand user-pass 1 (k k))
  (deflistener k)
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 2) (2 1)) ((3 2) (6 0))
    ((4 0) (2 0)) ((5 0) (1 2)) ((6 1) (0 1)))
  (uniq-orig k n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (1 1)) ((3 1) (1 0)) ((3 1) (2 1)))
  (rule eff-dev-up-1 power-deliver-once trRl_dev-up-at-1)
  (operation nonce-test (added-strand dev-up 2) k (6 0)
    (ch-msg start-ch (cat "power-up" o k)))
  (strand-map 0 1 2 3 4 5 6)
  (traces ((send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send (enc "open" d o n-0 k))) ((send (enc "may I pass" k)))
    ((recv k) (send k)))
  (label 24)
  (parent 22)
  (unrealized (6 0))
  (dead)
  (maps ((0 1) ((k k) (o o) (start-ch start-ch) (n n) (d d) (o-0 o))))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol subatomic-open-closed basic
  (defrole dev-up
    (vars (k skey) (d dev) (o name) (start-ch chan))
    (trace (recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send (enc "up" k)))
    (auth start-ch))
  (defrole owner-power-dev
    (vars (k skey) (o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "open" d o n k)) (recv n)))
  (defrole owner-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (send (enc "close" d o n k)) (recv n)))
  (defrole dev-open
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "open" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o o)) (send n))
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole dev-close
    (vars (k skey) (n text) (d dev) (o name))
    (trace (recv (enc "close" d o n k))
      (load (cat d "lk") (cat "st-k" o k))
      (stor (cat d "ls") (cat "st" o)) (send n))
    (gen-st (cat "st-k" o k)))
  (defrole dev-pass
    (vars (k skey) (n text) (d dev) (o name))
    (trace (load (cat d "lk") (cat "st-k" o k))
      (load (cat d "ls") (cat "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    (uniq-orig n)
    (gen-st (cat "st-k" o k) (cat "st" (cat o o))))
  (defrole user-pass
    (vars (k skey))
    (trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z2 (idx 2)) (p "dev-up" z1 (idx 2))
          (p "dev-up" "k" z2 k) (p "dev-up" "k" z1 k))
        (= z1 z2))))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1)
          (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule discreteBefore
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 2)) (trans z (idx 1)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_dev-close-at-2
    (forall ((z strd))
      (implies (p "dev-close" z (idx 3)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-up" z (idx 2)) (prec z (idx 1) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 3)) (prec z (idx 2) z1 i))))))
  (defgenrule cau-dev-pass-1
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule eff-dev-pass-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "dev-pass" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "dev-pass" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule gen-st-dev-open-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-open" z (idx 1)) (p "dev-open" "o" z o))
        (gen-st (cat "st" o o)))))
  (defgenrule gen-st-dev-close-0
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-close" z (idx 1)) (p "dev-close" "k" z k)
          (p "dev-close" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (o name) (k skey))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o)) (gen-st (cat "st-k" o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (o name))
      (implies (and (p "dev-pass" z (idx 1)) (p "dev-pass" "o" z o))
        (gen-st (cat "st" o o))))))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pval))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (uniq-orig n)
  (facts (no-state-split))
  (traces
    ((load (cat d "lk") (cat pt "st-k" o k))
      (load (cat d "ls") (cat pt-0 "st" o o))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 25)
  (realized)
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (n (0 3)))
  (comment "Not closed under rules"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pval))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (facts (no-state-split))
  (rule gen-st-dev-pass-0 gen-st-dev-pass-1)
  (traces
    ((load (cat d "lk") (cat pt "st-k" o k))
      (load (cat d "ls") (cat pt-0 "st" o o))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k))))
  (label 26)
  (parent 25)
  (unrealized (0 0) (0 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (n (0 3)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((1 2) (0 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((1 1) (0 0)))
  (rule eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o k)) (0 0))
  (strand-map 0)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 27)
  (parent 26)
  (unrealized (0 1) (1 0))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (precedes ((1 2) (0 0)) ((2 0) (1 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((1 1) (0 0)))
  (operation channel-test (added-strand owner-power-dev 1)
    (ch-msg start-ch (cat "power-up" o k)) (1 0))
  (strand-map 0 1)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send start-ch (cat "power-up" o k))))
  (label 28)
  (parent 27)
  (unrealized (0 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k k-0 skey) (n n-0 text) (o name)
    (pt pt-0 pt-1 pt-2 pval) (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (defstrand dev-open 3 (d d) (k k-0) (n n-0) (o o))
  (precedes ((1 2) (3 1)) ((2 0) (1 0)) ((3 2) (0 0)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k) (cat "st-k" o k-0))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((1 1) (0 0)) ((3 2) (0 1)))
  (rule cau-dev-pass-1 discreteBefore gen-st-dev-open-1
    trRl_dev-open-at-2)
  (operation channel-test (added-strand dev-open 3)
    (ch-msg (cat d "ls") (cat pt "st" o o)) (0 1))
  (strand-map 0 1 2)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o)))
    ((send start-ch (cat "power-up" o k)))
    ((recv (enc "open" d o n-0 k-0))
      (load (cat d "lk") (cat pt-2 "st-k" o k-0))
      (stor (cat d "ls") (cat pt "st" o o))))
  (label 29)
  (parent 28)
  (unrealized (3 1))
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton subatomic-open-closed
  (vars (d dev) (k skey) (n n-0 text) (o name) (pt pt-0 pt-1 pval)
    (start-ch chan))
  (defstrand dev-pass 4 (d d) (k k) (n n) (o o))
  (defstrand owner-power-dev 1 (k k) (o o) (start-ch start-ch))
  (defstrand dev-open 3 (d d) (k k) (n n-0) (o o))
  (defstrand dev-up 3 (d d) (k k) (o o) (start-ch start-ch))
  (precedes ((1 0) (3 0)) ((2 2) (0 0)) ((3 2) (2 1)))
  (uniq-orig n)
  (gen-st (cat "st" o o) (cat "st-k" o k))
  (conf start-ch)
  (auth start-ch)
  (facts (no-state-split))
  (leads-to ((2 2) (0 1)) ((3 1) (0 0)) ((3 1) (2 1)))
  (rule discreteBefore eff-dev-up-1 trRl_dev-up-at-1 trRl_dev-up-at-2)
  (operation channel-test (added-strand dev-up 2)
    (ch-msg (cat d "lk") (cat pt-0 "st-k" o k)) (3 1))
  (strand-map 0 2 3 1)
  (traces
    ((load (cat d "lk") (cat pt-0 "st-k" o k))
      (load (cat d "ls") (cat pt "st" o o)) (recv (enc "may I pass" k))
      (send (enc "you may pass" n k)))
    ((send start-ch (cat "power-up" o k)))
    ((recv (enc "open" d o n-0 k))
      (load (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt "st" o o)))
    ((recv start-ch (cat "power-up" o k))
      (stor (cat d "lk") (cat pt-0 "st-k" o k))
      (stor (cat d "ls") (cat pt-1 "st" o))))
  (label 30)
  (parent 29)
  (realized)
  (shape)
  (maps ((0) ((k k) (n n) (d d) (o o))))
  (origs (pt-0 (3 1)) (pt-1 (3 2)) (pt (2 2)) (n (0 3))))

(comment "Nothing left to do")