---

Protocol1(bss) ==
  A.es:EO+(Info)
       (Honest(A)
        (e:Act
             ((loc(e) = A)
              ((thr:Thread
                   (e  thr  (thr is one of bss at A)  loc(thr)= A))
                 (thr1,thr2:Thread.
                     (e  thr1
                      (thr1 is one of bss at A)
                      e  thr2
                      (thr2 is one of bss at A)
                      (thr1  thr2  thr2  thr1)))))))

---

Definitions :  lambda: x.A[x],  event-ordering+: EO+(Info),  ses-info: Info,  ses-honest: Honest(A),  equal: s = t,  Id: Id,  es-loc: loc(e),  exists: x:A. B[x],  and: P  Q,  ses-thread-loc: loc(thr)= A,  all: x:A. B[x],  ses-thread: Thread,  ses-thread-member: e  thr,  implies: P  Q,  ses-protocol1-thread: (thr is one of bss at A),  or: P  Q,  iseg: l1  l2,  ses-act: Act
FDL editor aliases :  ses-protocol1

---

Protocol1(bss)  ==
    \mlambda{}A.\mforall{}es:EO+(Info)
              (Honest(A)
              {}\mRightarrow{}  (\mforall{}e:Act
                          ((loc(e)  =  A)
                          {}\mRightarrow{}  ((\mexists{}thr:Thread.  (e  \mmember{}  thr  \mwedge{}  (thr  is  one  of  bss  at  A)  \mwedge{}  loc(thr)=  A))
                                \mwedge{}  (\mforall{}thr1,thr2:Thread.
                                          (e  \mmember{}  thr1
                                          {}\mRightarrow{}  (thr1  is  one  of  bss  at  A)
                                          {}\mRightarrow{}  e  \mmember{}  thr2
                                          {}\mRightarrow{}  (thr2  is  one  of  bss  at  A)
                                          {}\mRightarrow{}  (thr1  \mleq{}  thr2  \mvee{}  thr2  \mleq{}  thr1)))))))


Date html generated: 2010_08_28-AM-03_14_26
Last ObjectModification: 2010_02_23-AM-11_06_40

Home Index