程序状态 outbuf 发送给邻居但是尚未传到的 msg;inbuf 已传递到但是尚未计算处理的 msg。由于假设计算不花时间,传递消息需要时间,初始状态 inbuf 为空,outbuf 不一定为空
转移系统:状态按离散步骤变化的系统
条件
安全性条件:某个性质在每个可到达的配置中都成立(坏事从不发生)
不变式 {P} → {P} 在每个初始配置中成立、每次转移配置中不变
P 总为真不一定是不变式
活跃性条件:某个性质在每次执行中某些可达配置中必须成立(最终好事发生)
满足安全性 ⇒ 执行;都满足 ⇒ 容许/合法执行
异步消息传递、同步消息传递模型
消息复杂度:容许执行上发送 msg 总数的最大值
时间复杂度
根 $p_r$ 发送 M 给所有孩子。其他结点收到父结点的 M 的时候把 M 发送给自己的所有孩子。
输入:根结点消息 <m>
输出:每个结点都收到 <m>
Pi code:
begin
while (receiving no msg) do
if i = r then
send <m> to all children
terminates
end if
end while
while (receiving <m> from Pj) do
send <m> to all children
terminates
end while
end