cpsa-4.4.4: tst/sa.scm

(defprotocol subatomic-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)
      (load ls old1) (stor lk (cat "st-k" d o k))
      (stor ls (cat "st" d o)) (send (enc "up" k)))
    (auth start-ch)
    (critical-sections (1 4))
    (facts (same-dev ls lk)))
  (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 ls (cat "st" d any))
      (load lk (cat "st-k" d o k)) (stor ls (cat "st" d o o)) (send n))
    (critical-sections (1 3))
    (gen-st (cat "st-k" d o k) (cat "st" d (cat o o)))
    (facts (same-dev ls lk)))
  (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))
    (gen-st (cat "st-k" d o k))
    (critical-sections (1 3))
    (facts (same-dev ls lk)))
  (defrole dev-pass
    (vars (k skey) (n text) (d o name) (lk ls locn))
    (trace (load lk (cat "st-k" d o k)) (load ls (cat "st" d o o))
      (recv (enc "may I pass" k)) (send (enc "you may pass" n k)))
    (uniq-orig n)
    (gen-st (cat "st-k" d o k) (cat "st" d (cat o o)))
    (critical-sections (0 1))
    (facts (same-dev ls lk)))
  (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" z1 (idx 2)) (p "dev-up" z2 (idx 2))
          (p "dev-up" "k" z1 k) (p "dev-up" "k" z2 k))
        (= z1 z2))))
  (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))))
  (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 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 fact-dev-up-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-up" z (idx 3)) (p "dev-up" "lk" z lk)
          (p "dev-up" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-open-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-open" z (idx 3)) (p "dev-open" "lk" z lk)
          (p "dev-open" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-close-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-close" z (idx 3)) (p "dev-close" "lk" z lk)
          (p "dev-close" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-pass-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "lk" z lk)
          (p "dev-pass" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule trRl_dev-up-at-4
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-up-at-3
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 1)))))
  (defgenrule trRl_dev-open-at-3
    (forall ((z strd))
      (implies (p "dev-open" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-open-at-1
    (forall ((z strd))
      (implies (p "dev-open" z (idx 4)) (trans z (idx 1)))))
  (defgenrule trRl_dev-close-at-3
    (forall ((z strd))
      (implies (p "dev-close" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-close-at-2
    (forall ((z strd))
      (implies (p "dev-close" z (idx 4)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 5)) (prec z (idx 4) z1 i))))))
  (defgenrule cau-dev-up-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-open-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-open" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-close-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-close" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-pass-1
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule gen-st-dev-open-1
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o) (p "dev-open" "d" z d))
        (gen-st (cat "st-k" d o k)))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (o d name))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "o" z o)
          (p "dev-open" "d" z d)) (gen-st (cat "st" d o o)))))
  (defgenrule gen-st-dev-close-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-close" z (idx 1)) (p "dev-close" "k" z k)
          (p "dev-close" "o" z o) (p "dev-close" "d" z d))
        (gen-st (cat "st-k" d o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o) (p "dev-pass" "d" z d))
        (gen-st (cat "st-k" d o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (o d name))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "o" z o)
          (p "dev-pass" "d" z d)) (gen-st (cat "st" d o o))))))


(defgoal subatomic-open-closed
  (forall
    ((k skey) (n text) (d o d-0 o-0 name) (start-ch chan) (lk ls locn)
      (z z-0 strd))
    (implies
      (and (p "owner-power-dev" z 2) (p "dev-pass" z-0 4)
        (p "owner-power-dev" "k" z k) (p "owner-power-dev" "d" z d)
        (p "owner-power-dev" "o" z o)
        (p "owner-power-dev" "start-ch" z start-ch)
        (p "dev-pass" "k" z-0 k) (p "dev-pass" "n" z-0 n)
        (p "dev-pass" "d" z-0 d-0) (p "dev-pass" "o" z-0 o-0)
        (p "dev-pass" "lk" z-0 lk) (p "dev-pass" "ls" z-0 ls)
        (uniq-at n z-0 3) (uniq-at k z 0) (conf start-ch)
        (fact no-state-split))
      (exists ((any old old1 mesg) (n-0 text) (z-1 z-2 z-3 z-4 strd))
        (and (= d-0 d) (= o-0 o) (p "dev-open" z-1 4)
          (p "owner-open" z-2 1) (p "user-pass" z-3 1)
          (p "dev-up" z-4 6) (p "dev-pass" "d" z-0 d)
          (p "dev-pass" "o" z-0 o) (p "dev-open" "any" z-1 any)
          (p "dev-open" "k" z-1 k) (p "dev-open" "n" z-1 n-0)
          (p "dev-open" "d" z-1 d) (p "dev-open" "o" z-1 o)
          (p "dev-open" "lk" z-1 lk) (p "dev-open" "ls" z-1 ls)
          (p "owner-open" "k" z-2 k) (p "owner-open" "n" z-2 n-0)
          (p "owner-open" "d" z-2 d) (p "owner-open" "o" z-2 o)
          (p "user-pass" "k" z-3 k) (p "dev-up" "old" z-4 old)
          (p "dev-up" "old1" z-4 old1) (p "dev-up" "k" z-4 k)
          (p "dev-up" "d" z-4 d) (p "dev-up" "o" z-4 o)
          (p "dev-up" "start-ch" z-4 start-ch) (p "dev-up" "lk" z-4 lk)
          (p "dev-up" "ls" z-4 ls) (prec z 0 z-4 0) (prec z-1 3 z-0 0)
          (prec z-2 0 z-1 0) (prec z-3 0 z-0 2) (prec z-4 4 z-1 1)
          (prec z-4 5 z 1) (gen-st (cat "st" d o o))
          (gen-st (cat "st-k" d o k)) (leads-to z-1 3 z-0 1)
          (leads-to z-4 3 z-0 0) (leads-to z-4 3 z-1 2) (auth start-ch)
          (fact same-dev ls lk))))))