Nuprl Definition : nysiad_main
nysiad_main(M;actors;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;...;mf;...;X) ==
nysiad_Replicas(actors;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf;X)
|| nysiad_MessageBag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;...;mf;...)
|| nysiad_OnReceiptMsg(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;senders;...;mf)@actors
Definitions occuring in Statement :
nysiad_OnReceiptMsg: nysiad_OnReceiptMsg(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;senders;tooarcasthdr;mf),
nysiad_Replicas: nysiad_Replicas(actors;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf;X),
nysiad_MessageBag: nysiad_MessageBag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;senders;...;...;mf;msg2m),
class-at: X@locs,
parallel-class: X || Y
FDL editor aliases :
nysiad_main
Latex:
nysiad\_main(M;actors;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;...;...;...;...;mf;...;X) ==
nysiad\_Replicas(actors;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;mf;X)
|| nysiad\_MessageBag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;...;...;...;...;mf;msg2m)
|| nysiad\_OnReceiptMsg(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;...;mf)@actors
Date html generated:
2015_07_23-PM-03_48_11
Last ObjectModification:
2014_08_06-PM-03_36_26
Home
Index