cpsa-4.4.4: tst/atomic-open-closed_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald atomic-open-closed (bound 44))
(comment "CPSA 4.3.1")
(comment "All input read from tst/atomic-open-closed.scm")
(comment "Strand count bounded at 44")
(defprotocol atomic-open-closed basic
(defrole dev-up
(vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
(lk ls locn))
(trace (recv start-ch (cat "power-up" d o k)) (load lk old)
(stor lk (cat "st-k" d o k)) (load ls old1)
(stor ls (cat "st" d o)) (send (enc "up" k)))
(auth start-ch))
(defrole owner-power-dev
(vars (k skey) (d o name) (start-ch chan))
(trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
(conf start-ch))
(defrole owner-open
(vars (k skey) (n text) (d o name))
(trace (send (enc "open" d o n k)) (recv n)))
(defrole owner-close
(vars (k skey) (n text) (d o name))
(trace (send (enc "close" d o n k)) (recv n)))
(defrole dev-open
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "open" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o o)) (send n)))
(defrole dev-close
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "close" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o)) (send n)))
(defrole dev-pass
(vars (k skey) (n text) (d o name) (lk ls locn))
(trace (recv (enc "may I pass" k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d o o)) (send (enc "you may pass" n k)))
(uniq-orig n))
(defrole user-pass
(vars (k skey))
(trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
(defrule gen-state-close
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-close" z 1) (p "dev-close" "d" z d)
(p "dev-close" "o" z o) (p "dev-close" "k" z k)
(p "dev-close" "any" z (cat o o)))
(gen-st (cat "st" d o o)))))
(defrule gen-state-pass
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-pass" z 1) (p "dev-pass" "d" z d)
(p "dev-pass" "o" z o) (p "dev-pass" "k" z k))
(gen-st (cat "st" d o o)))))
(defrule gen-state-open
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-open" "d" z d) (p "dev-open" "o" z o)
(p "dev-open" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-close
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-close" "d" z d) (p "dev-close" "o" z o)
(p "dev-close" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-pass
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-pass" "d" z d) (p "dev-pass" "o" z o)
(p "dev-pass" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule power-deliver-once
(forall ((z1 z2 strd) (k skey))
(implies
(and (p "dev-up" z1 2) (p "dev-up" z2 2) (p "dev-up" "k" z1 k)
(p "dev-up" "k" z2 k))
(= z1 z2))))
(defrule intro-same-dev-up
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-up" "lk" z lk) (p "dev-up" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-open
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-open" "lk" z lk) (p "dev-open" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-close
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-close" "lk" z lk) (p "dev-close" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-pass
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-pass" "lk" z lk) (p "dev-pass" "ls" z ls))
(fact same-dev ls lk))))
(defrule same-dev-ls-lk
(forall ((ls lk lk-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls lk-0))
(= lk lk-0))))
(defrule same-dev-lk-ls
(forall ((lk ls ls-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls-0 lk))
(= ls ls-0))))
(defrule single-thread-up-up
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-up" y 5) (p "dev-up" "lk" x lk)
(p "dev-up" "lk" y lk))
(or (= x y) (prec x 4 y 1) (prec y 4 x 1)))))
(defrule single-thread-up-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-open" y 4) (p "dev-up" "ls" x ls)
(p "dev-open" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-up-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-close" y 4) (p "dev-up" "ls" x ls)
(p "dev-close" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-open-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-open" y 4)
(p "dev-open" "ls" x ls) (p "dev-open" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-ls-open-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-close" y 4)
(p "dev-open" "ls" x ls) (p "dev-close" "ls" y ls))
(or (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-close-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-close" x 4) (p "dev-close" y 4)
(p "dev-close" "ls" x ls) (p "dev-close" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule atomic-up-pass
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-pass" y 3) (p "dev-up" "lk" x lk)
(p "dev-pass" "lk" y lk) (prec x 2 y 1))
(prec x 4 y 1))))
(defrule dev-up-completes
(forall ((x strd)) (implies (p "dev-up" x 2) (p "dev-up" x 5))))
(defrule dev-open-completes
(forall ((x strd)) (implies (p "dev-open" x 2) (p "dev-open" x 4))))
(defrule dev-close-completes
(forall ((x strd))
(implies (p "dev-close" x 2) (p "dev-close" x 4))))
(defrule dev-pass-completes
(forall ((x strd)) (implies (p "dev-pass" x 2) (p "dev-pass" x 3))))
(defrule dev-up-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec x i1 z 4))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-up-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec z 1 x i1))
(or (= x z) (prec z 4 x i1)))))
(defrule dev-open-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-open-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-close-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-close-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-pass-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec x i1 z 2))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-pass-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec z 1 x i1))
(or (= x z) (prec z 2 x i1)))))
(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 shearsRule
(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) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(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-4
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 4))))
(defgenrule trRl_dev-up-at-3
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 3))))
(defgenrule trRl_dev-up-at-2
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 2))))
(defgenrule trRl_dev-up-at-1
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 1))))
(defgenrule trRl_dev-open-at-3
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 3))))
(defgenrule trRl_dev-open-at-2
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 2))))
(defgenrule trRl_dev-close-at-3
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 3))))
(defgenrule trRl_dev-close-at-2
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 2))))
(defgenrule cau-dev-open-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-open" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-close-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-close" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-pass-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-pass" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1))))))
(defskeleton atomic-open-closed
(vars (k skey) (d o name) (start-ch chan))
(defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
(deflistener k)
(uniq-orig k)
(conf start-ch)
(traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
((recv k) (send k)))
(label 0)
(unrealized (0 1) (1 0))
(preskeleton)
(origs (k (0 0)))
(comment "Not a skeleton"))
(comment "Nothing left to do")
(defprotocol atomic-open-closed basic
(defrole dev-up
(vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
(lk ls locn))
(trace (recv start-ch (cat "power-up" d o k)) (load lk old)
(stor lk (cat "st-k" d o k)) (load ls old1)
(stor ls (cat "st" d o)) (send (enc "up" k)))
(auth start-ch))
(defrole owner-power-dev
(vars (k skey) (d o name) (start-ch chan))
(trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
(conf start-ch))
(defrole owner-open
(vars (k skey) (n text) (d o name))
(trace (send (enc "open" d o n k)) (recv n)))
(defrole owner-close
(vars (k skey) (n text) (d o name))
(trace (send (enc "close" d o n k)) (recv n)))
(defrole dev-open
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "open" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o o)) (send n)))
(defrole dev-close
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "close" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o)) (send n)))
(defrole dev-pass
(vars (k skey) (n text) (d o name) (lk ls locn))
(trace (recv (enc "may I pass" k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d o o)) (send (enc "you may pass" n k)))
(uniq-orig n))
(defrole user-pass
(vars (k skey))
(trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
(defrule gen-state-close
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-close" z 1) (p "dev-close" "d" z d)
(p "dev-close" "o" z o) (p "dev-close" "k" z k)
(p "dev-close" "any" z (cat o o)))
(gen-st (cat "st" d o o)))))
(defrule gen-state-pass
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-pass" z 1) (p "dev-pass" "d" z d)
(p "dev-pass" "o" z o) (p "dev-pass" "k" z k))
(gen-st (cat "st" d o o)))))
(defrule gen-state-open
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-open" "d" z d) (p "dev-open" "o" z o)
(p "dev-open" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-close
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-close" "d" z d) (p "dev-close" "o" z o)
(p "dev-close" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-pass
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-pass" "d" z d) (p "dev-pass" "o" z o)
(p "dev-pass" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule power-deliver-once
(forall ((z1 z2 strd) (k skey))
(implies
(and (p "dev-up" z1 2) (p "dev-up" z2 2) (p "dev-up" "k" z1 k)
(p "dev-up" "k" z2 k))
(= z1 z2))))
(defrule intro-same-dev-up
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-up" "lk" z lk) (p "dev-up" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-open
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-open" "lk" z lk) (p "dev-open" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-close
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-close" "lk" z lk) (p "dev-close" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-pass
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-pass" "lk" z lk) (p "dev-pass" "ls" z ls))
(fact same-dev ls lk))))
(defrule same-dev-ls-lk
(forall ((ls lk lk-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls lk-0))
(= lk lk-0))))
(defrule same-dev-lk-ls
(forall ((lk ls ls-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls-0 lk))
(= ls ls-0))))
(defrule single-thread-up-up
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-up" y 5) (p "dev-up" "lk" x lk)
(p "dev-up" "lk" y lk))
(or (= x y) (prec x 4 y 1) (prec y 4 x 1)))))
(defrule single-thread-up-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-open" y 4) (p "dev-up" "ls" x ls)
(p "dev-open" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-up-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-close" y 4) (p "dev-up" "ls" x ls)
(p "dev-close" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-open-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-open" y 4)
(p "dev-open" "ls" x ls) (p "dev-open" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-ls-open-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-close" y 4)
(p "dev-open" "ls" x ls) (p "dev-close" "ls" y ls))
(or (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-close-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-close" x 4) (p "dev-close" y 4)
(p "dev-close" "ls" x ls) (p "dev-close" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule atomic-up-pass
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-pass" y 3) (p "dev-up" "lk" x lk)
(p "dev-pass" "lk" y lk) (prec x 2 y 1))
(prec x 4 y 1))))
(defrule dev-up-completes
(forall ((x strd)) (implies (p "dev-up" x 2) (p "dev-up" x 5))))
(defrule dev-open-completes
(forall ((x strd)) (implies (p "dev-open" x 2) (p "dev-open" x 4))))
(defrule dev-close-completes
(forall ((x strd))
(implies (p "dev-close" x 2) (p "dev-close" x 4))))
(defrule dev-pass-completes
(forall ((x strd)) (implies (p "dev-pass" x 2) (p "dev-pass" x 3))))
(defrule dev-up-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec x i1 z 4))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-up-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec z 1 x i1))
(or (= x z) (prec z 4 x i1)))))
(defrule dev-open-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-open-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-close-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-close-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-pass-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec x i1 z 2))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-pass-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec z 1 x i1))
(or (= x z) (prec z 2 x i1)))))
(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 shearsRule
(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) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(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-4
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 4))))
(defgenrule trRl_dev-up-at-3
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 3))))
(defgenrule trRl_dev-up-at-2
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 2))))
(defgenrule trRl_dev-up-at-1
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 1))))
(defgenrule trRl_dev-open-at-3
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 3))))
(defgenrule trRl_dev-open-at-2
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 2))))
(defgenrule trRl_dev-close-at-3
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 3))))
(defgenrule trRl_dev-close-at-2
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 2))))
(defgenrule cau-dev-open-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-open" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-close-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-close" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-pass-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-pass" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1))))))
(defskeleton atomic-open-closed
(vars (k skey) (n text) (d o name) (pt pt-0 pval) (lk ls locn))
(defstrand dev-pass 4 (k k) (n n) (d d) (o o) (lk lk) (ls ls))
(uniq-orig n)
(traces
((recv (enc "may I pass" k)) (load lk (cat pt "st-k" d o k))
(load ls (cat pt-0 "st" d o o)) (send (enc "you may pass" n k))))
(label 3)
(realized)
(origs (n (0 3)))
(comment "Not closed under rules"))
(defskeleton atomic-open-closed
(vars (old old1 any mesg) (k skey) (n n-0 text) (d o name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (start-ch chan) (ls lk locn))
(defstrand dev-pass 4 (k k) (n n) (d d) (o o) (lk lk) (ls ls))
(defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
(start-ch start-ch) (lk lk) (ls ls))
(defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
(defstrand dev-open 4 (any any) (k k) (n n-0) (d d) (o o) (lk lk)
(ls ls))
(precedes ((1 4) (3 1)) ((2 0) (1 0)) ((3 3) (0 1)))
(uniq-orig n)
(gen-st (cat "st" d o o) (cat "st-k" d o k))
(conf start-ch)
(auth start-ch)
(facts (same-dev ls lk) (trans 3 3) (trans 3 2) (trans 1 4)
(trans 1 3) (trans 1 2) (trans 1 1))
(operation channel-test (displaced 4 1 dev-up 3)
(ch-msg lk (cat pt-5 "st-k" d o k-0)) (3 1))
(traces
((recv (enc "may I pass" k)) (load lk (cat pt-1 "st-k" d o k))
(load ls (cat pt "st" d o o)) (send (enc "you may pass" n k)))
((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
(stor lk (cat pt-1 "st-k" d o k)) (load ls (cat pt-2 old1))
(stor ls (cat pt-3 "st" d o)))
((send start-ch (cat "power-up" d o k)))
((recv (enc "open" d o n-0 k)) (load lk (cat pt-1 "st-k" d o k))
(load ls (cat pt-4 "st" d any)) (stor ls (cat pt "st" d o o))))
(label 8)
(parent 3)
(realized)
(shape)
(maps
((0) ((k k) (n n) (d d) (o o) (lk lk) (ls ls) (pt pt-1) (pt-0 pt))))
(origs (pt-1 (1 2)) (pt (3 3)) (pt-3 (1 4)) (n (0 3))))
(comment "Nothing left to do")
(defprotocol atomic-open-closed basic
(defrole dev-up
(vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
(lk ls locn))
(trace (recv start-ch (cat "power-up" d o k)) (load lk old)
(stor lk (cat "st-k" d o k)) (load ls old1)
(stor ls (cat "st" d o)) (send (enc "up" k)))
(auth start-ch))
(defrole owner-power-dev
(vars (k skey) (d o name) (start-ch chan))
(trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
(conf start-ch))
(defrole owner-open
(vars (k skey) (n text) (d o name))
(trace (send (enc "open" d o n k)) (recv n)))
(defrole owner-close
(vars (k skey) (n text) (d o name))
(trace (send (enc "close" d o n k)) (recv n)))
(defrole dev-open
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "open" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o o)) (send n)))
(defrole dev-close
(vars (k skey) (n text) (any mesg) (d o name) (lk ls locn))
(trace (recv (enc "close" d o n k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d any)) (stor ls (cat "st" d o)) (send n)))
(defrole dev-pass
(vars (k skey) (n text) (d o name) (lk ls locn))
(trace (recv (enc "may I pass" k)) (load lk (cat "st-k" d o k))
(load ls (cat "st" d o o)) (send (enc "you may pass" n k)))
(uniq-orig n))
(defrole user-pass
(vars (k skey))
(trace (send (enc "may I pass" k)) (recv (enc "you may pass" k))))
(defrule gen-state-close
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-close" z 1) (p "dev-close" "d" z d)
(p "dev-close" "o" z o) (p "dev-close" "k" z k)
(p "dev-close" "any" z (cat o o)))
(gen-st (cat "st" d o o)))))
(defrule gen-state-pass
(forall ((z strd) (d o name) (k skey))
(implies
(and (p "dev-pass" z 1) (p "dev-pass" "d" z d)
(p "dev-pass" "o" z o) (p "dev-pass" "k" z k))
(gen-st (cat "st" d o o)))))
(defrule gen-state-open
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-open" "d" z d) (p "dev-open" "o" z o)
(p "dev-open" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-close
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-close" "d" z d) (p "dev-close" "o" z o)
(p "dev-close" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule gen-state-pass
(forall ((z strd) (d o k mesg))
(implies
(and (p "dev-pass" "d" z d) (p "dev-pass" "o" z o)
(p "dev-pass" "k" z k))
(gen-st (cat "st-k" d o k)))))
(defrule power-deliver-once
(forall ((z1 z2 strd) (k skey))
(implies
(and (p "dev-up" z1 2) (p "dev-up" z2 2) (p "dev-up" "k" z1 k)
(p "dev-up" "k" z2 k))
(= z1 z2))))
(defrule intro-same-dev-up
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-up" "lk" z lk) (p "dev-up" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-open
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-open" "lk" z lk) (p "dev-open" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-close
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-close" "lk" z lk) (p "dev-close" "ls" z ls))
(fact same-dev ls lk))))
(defrule intro-same-dev-pass
(forall ((z strd) (lk ls locn))
(implies
(and (p "dev-pass" "lk" z lk) (p "dev-pass" "ls" z ls))
(fact same-dev ls lk))))
(defrule same-dev-ls-lk
(forall ((ls lk lk-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls lk-0))
(= lk lk-0))))
(defrule same-dev-lk-ls
(forall ((lk ls ls-0 locn))
(implies
(and (fact same-dev ls lk) (fact same-dev ls-0 lk))
(= ls ls-0))))
(defrule single-thread-up-up
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-up" y 5) (p "dev-up" "lk" x lk)
(p "dev-up" "lk" y lk))
(or (= x y) (prec x 4 y 1) (prec y 4 x 1)))))
(defrule single-thread-up-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-open" y 4) (p "dev-up" "ls" x ls)
(p "dev-open" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-up-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-up" x 5) (p "dev-close" y 4) (p "dev-up" "ls" x ls)
(p "dev-close" "ls" y ls))
(or (prec x 4 y 1) (prec y 3 x 1)))))
(defrule single-thread-open-open
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-open" y 4)
(p "dev-open" "ls" x ls) (p "dev-open" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-ls-open-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-open" x 4) (p "dev-close" y 4)
(p "dev-open" "ls" x ls) (p "dev-close" "ls" y ls))
(or (prec x 3 y 1) (prec y 3 x 1)))))
(defrule single-thread-close-close
(forall ((x y strd) (ls locn))
(implies
(and (p "dev-close" x 4) (p "dev-close" y 4)
(p "dev-close" "ls" x ls) (p "dev-close" "ls" y ls))
(or (= x y) (prec x 3 y 1) (prec y 3 x 1)))))
(defrule atomic-up-pass
(forall ((x y strd) (lk locn))
(implies
(and (p "dev-up" x 5) (p "dev-pass" y 3) (p "dev-up" "lk" x lk)
(p "dev-pass" "lk" y lk) (prec x 2 y 1))
(prec x 4 y 1))))
(defrule dev-up-completes
(forall ((x strd)) (implies (p "dev-up" x 2) (p "dev-up" x 5))))
(defrule dev-open-completes
(forall ((x strd)) (implies (p "dev-open" x 2) (p "dev-open" x 4))))
(defrule dev-close-completes
(forall ((x strd))
(implies (p "dev-close" x 2) (p "dev-close" x 4))))
(defrule dev-pass-completes
(forall ((x strd)) (implies (p "dev-pass" x 2) (p "dev-pass" x 3))))
(defrule dev-up-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec x i1 z 4))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-up-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-up" z 5) (prec z 1 x i1))
(or (= x z) (prec z 4 x i1)))))
(defrule dev-open-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-open-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-open" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-close-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec x i1 z 3))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-close-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-close" z 4) (prec z 1 x i1))
(or (= x z) (prec z 3 x i1)))))
(defrule dev-pass-atomic1
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec x i1 z 2))
(or (= x z) (prec x i1 z 1)))))
(defrule dev-pass-atomic2
(forall ((x z strd) (i1 indx))
(implies
(and (p "dev-pass" z 3) (prec z 1 x i1))
(or (= x z) (prec z 2 x i1)))))
(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 shearsRule
(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) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(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-4
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 4))))
(defgenrule trRl_dev-up-at-3
(forall ((z strd)) (implies (p "dev-up" z 5) (trans z 3))))
(defgenrule trRl_dev-up-at-2
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 2))))
(defgenrule trRl_dev-up-at-1
(forall ((z strd)) (implies (p "dev-up" z 3) (trans z 1))))
(defgenrule trRl_dev-open-at-3
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 3))))
(defgenrule trRl_dev-open-at-2
(forall ((z strd)) (implies (p "dev-open" z 4) (trans z 2))))
(defgenrule trRl_dev-close-at-3
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 3))))
(defgenrule trRl_dev-close-at-2
(forall ((z strd)) (implies (p "dev-close" z 4) (trans z 2))))
(defgenrule cau-dev-open-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-open" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-close-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-close" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1)))))
(defgenrule cau-dev-pass-2
(forall ((z z1 strd) (i indx))
(implies (and (p "dev-pass" z 3) (prec z1 i z 2))
(or (= z z1) (prec z1 i z 1))))))
(defskeleton atomic-open-closed
(vars (k skey) (n text) (d o d-0 o-0 name) (pt pt-0 pval)
(start-ch chan) (lk ls locn))
(defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
(defstrand dev-pass 4 (k k) (n n) (d d-0) (o o-0) (lk lk) (ls ls))
(uniq-orig k n)
(conf start-ch)
(traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
((recv (enc "may I pass" k)) (load lk (cat pt "st-k" d-0 o-0 k))
(load ls (cat pt-0 "st" d-0 o-0 o-0))
(send (enc "you may pass" n k))))
(label 9)
(unrealized (0 1) (1 0) (1 1))
(preskeleton)
(origs (n (1 3)) (k (0 0)))
(comment "Not a skeleton"))
(defskeleton atomic-open-closed
(vars (any old old1 mesg) (k skey) (n n-0 text) (d o name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (start-ch chan) (lk ls locn))
(defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
(defstrand dev-pass 4 (k k) (n n) (d d) (o o) (lk lk) (ls ls))
(defstrand user-pass 1 (k k))
(defstrand dev-open 4 (any any) (k k) (n n-0) (d d) (o o) (lk lk)
(ls ls))
(defstrand owner-open 1 (k k) (n n-0) (d d) (o o))
(defstrand dev-up 6 (old old) (old1 old1) (k k) (d d) (o o)
(start-ch start-ch) (lk lk) (ls ls))
(precedes ((0 0) (5 0)) ((2 0) (1 0)) ((3 3) (1 1)) ((4 0) (3 0))
((5 4) (3 1)) ((5 5) (0 1)))
(uniq-orig k n)
(gen-st (cat "st" d o o) (cat "st-k" d o k))
(conf start-ch)
(auth start-ch)
(facts (same-dev ls lk) (trans 3 3) (trans 3 2) (trans 5 4)
(trans 5 3) (trans 5 2) (trans 5 1))
(operation encryption-test (displaced 3 6 dev-up 6) (enc "up" k)
(0 1))
(traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
((recv (enc "may I pass" k)) (load lk (cat pt-2 "st-k" d o k))
(load ls (cat pt "st" d o o)) (send (enc "you may pass" n k)))
((send (enc "may I pass" k)))
((recv (enc "open" d o n-0 k)) (load lk (cat pt-2 "st-k" d o k))
(load ls (cat pt-0 "st" d any)) (stor ls (cat pt "st" d o o)))
((send (enc "open" d o n-0 k)))
((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-1 old))
(stor lk (cat pt-2 "st-k" d o k)) (load ls (cat pt-3 old1))
(stor ls (cat pt-4 "st" d o)) (send (enc "up" k))))
(label 21)
(parent 9)
(realized)
(shape)
(maps
((0 1)
((k k) (d d) (o o) (start-ch start-ch) (n n) (d-0 d) (o-0 o)
(lk lk) (ls ls) (pt pt-2) (pt-0 pt))))
(origs (pt-2 (5 2)) (pt-4 (5 4)) (pt (3 3)) (n (1 3)) (k (0 0))))
(comment "Nothing left to do")