---

StandardMessageAutomaton(X;hdrs) ==
  message-constraint{i:l}(es;X;hdrs)  messages-delivered{i:l}(es;X)

---

Definitions occuring in Statement :  message-constraint: message-constraint{i:l}(es;X;hdrs),  messages-delivered: messages-delivered{i:l}(es;X),  and: P  Q
Definitions :  and: P  Q,  message-constraint: message-constraint{i:l}(es;X;hdrs),  messages-delivered: messages-delivered{i:l}(es;X)
FDL editor aliases :  std-ma

---

StandardMessageAutomaton(X;hdrs)  ==
    message-constraint\{i:l\}(es;X;hdrs)  \mwedge{}  messages-delivered\{i:l\}(es;X)


Date html generated: 2011_08_17-PM-04_06_40
Last ObjectModification: 2011_05_12-PM-06_51_46

Home Index