---

Comm-next-selex(l_comm;piD;cSt) ==
  let rndv = pDVselex-rndv1(piD) in
   let val = snd(snd(snd(rndv))) in
   let i = fst(rndv) in
   let loc = fst(snd(rndv)) in
   let j = fst(snd(snd(rndv))) in
   let cSt' = fpf-restrict(Comm-st(cSt);x.(x = loc)) in
   <<cSt', Comm-q(cSt), Comm-req_from(cSt), ff, Comm-count(cSt)>
   , make-lg([<l_comm, mk-tagged("msg";pDVcontinue())>; 
              
              <Comm-req_from(cSt), mk-tagged("msg";pDVmsg(val;i))>;
               
              <loc, mk-tagged("msg";pDVmsg(val;j))>])
   >

---

Definitions :  pDVselex-rndv1: pDVselex-rndv1(x),  pi1: fst(t),  pi2: snd(t),  let: let,  fpf-restrict: fpf-restrict(f;P),  Comm-st: Comm-st(cSt),  lambda: x.A[x],  bnot: b,  eq_id: a = b,  Comm-q: Comm-q(cSt),  bfalse: ff,  Comm-count: Comm-count(cSt),  make-lg: make-lg(L),  pDVcontinue: pDVcontinue(),  Comm-req_from: Comm-req_from(cSt),  cons: [car / cdr],  pair: <a, b>,  mk-tagged: mk-tagged(tg;x),  token: "$token",  pDVmsg: pDVmsg(val;index),  nil: []
FDL editor aliases :  Comm-next-selex

---

Comm-next-selex(l$_{comm}$;piD;cSt)  ==
    let  rndv  =  pDVselex-rndv1(piD)  in
      let  val  =  snd(snd(snd(rndv)))  in
      let  i  =  fst(rndv)  in
      let  loc  =  fst(snd(rndv))  in
      let  j  =  fst(snd(snd(rndv)))  in
      let  cSt'  =  fpf-restrict(Comm-st(cSt);\mlambda{}x.(\mneg{}\msubb{}x  =  loc))  in
      <<cSt',  Comm-q(cSt),  Comm-req\_from(cSt),  ff,  Comm-count(cSt)>
      ,  make-lg([<l$_{comm}$,  mk-tagged("msg";pDVcontinue())> 
                           
                            <Comm-req\_from(cSt),  mk-tagged("msg";pDVmsg(val;i))>
                             
                            <loc,  mk-tagged("msg";pDVmsg(val;j))>])
      >


Date html generated: 2010_08_27-PM-09_38_04
Last ObjectModification: 2010_04_27-PM-03_37_50

Home Index