p.tr delivered at p)
p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q))e.
is-send(E)(e)
loc(E)(e) =
p;tr)
is mentioned by
|
Def local_deliver_property(E;P)(tr) == P(p.tr delivered at p) | [local_deliver_property] |
|
Def totalorder(E)(tr)
== p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q)) | [totalorder] |
Try larger context: GenAutomata