Nuprl Definition : mu_ex_v5_HandleUseSR

mu_ex_v5_HandleUseSR(initial_token;m1;m2;proc1;proc2) ==
  l.let F = l,zk,z.
              let interested,token,toreply = z in 
              if interested then {mu_ex_v5_send_busy() (mu_ex_v5_getMachine(m1;m2;proc1) l) }
              if token then {mu_ex_v5_send_enter_cs() (mu_ex_v5_getMachine(m1;m2;proc1) l) }
              else {mu_ex_v5_send_request() (mu_ex_v5_getOtherProc(proc1;proc2) l) }
              fi  in
         F@Loc|Loc,mu_ex_v5_UseSR(), mu_ex_v5_PrState(initial_token)|


Definitions occuring in Statement :  mu_ex_v5_PrState: mu_ex_v5_PrState(initial_token),  mu_ex_v5_getMachine: mu_ex_v5_getMachine(m1;m2;proc1),  mu_ex_v5_getOtherProc: mu_ex_v5_getOtherProc(proc1;proc2),  mu_ex_v5_send_busy: mu_ex_v5_send_busy(),  mu_ex_v5_UseSR: mu_ex_v5_UseSR(),  mu_ex_v5_send_enter_cs: mu_ex_v5_send_enter_cs(),  mu_ex_v5_send_request: mu_ex_v5_send_request(),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  ifthenelse: if b then t else f fi ,  let: let,  it: ,  spreadn: spread3,  apply: f a,  lambda: x.A[x],  single-bag: {x}
FDL editor aliases :  mu_ex_v5_HandleUseSR
mu\_ex\_v5\_HandleUseSR(initial$_{token}$;m1;m2;proc1;proc2)  ==
    \mlambda{}l.let  F  =  \mlambda{}l,zk,z.
                            let  interested,token,toreply  =  z  in 
                            if  interested  then  \{mu\_ex\_v5\_send\_busy()  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  l)  \mcdot{}\}
                            if  token  then  \{mu\_ex\_v5\_send\_enter\_cs()  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  l)  \mcdot{}\}
                            else  \{mu\_ex\_v5\_send\_request()  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  l)  \mcdot{}\}
                            fi    in
                  F@Loc|Loc,mu\_ex\_v5\_UseSR(),  mu\_ex\_v5\_PrState(initial$_{token}$)|


Date html generated: 2012_02_20-PM-06_55_41
Last ObjectModification: 2012_02_02-PM-02_58_59

Home Index