Nuprl Definition : std-ma-with-omissions
StandardMessageAutomaton(X;hdrs) (with send omissions at fail locations) ==
message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered-with-omissions{i:l}(es;X;fail;f)
Definitions occuring in Statement :
message-constraint: message-constraint{i:l}(es;X;hdrs;f),
messages-delivered-with-omissions: messages-delivered-with-omissions{i:l}(es;X;faults;f),
and: P ∧ Q
FDL editor aliases :
std-ma-with-omissions
Latex:
StandardMessageAutomaton(X;hdrs) (with send omissions at fail locations) ==
message-constraint\{i:l\}(es;X;hdrs;f) \mwedge{} messages-delivered-with-omissions\{i:l\}(es;X;fail;f)
Date html generated:
2015_07_21-PM-04_53_07
Last ObjectModification:
2013_02_27-PM-02_58_33
Home
Index