《表2 Basic Paxos的消息流》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于Coq的Paxos形式化建模与验证》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

在准备工作和投票行为建模完成之后，我们以文献[7]中的一个具体的算法例子来说明Paxos的实际情况和形式化定义之间的一致性.如表2所示，系统中包含5个参与者A，B，C，D和E，并且一共进行了5个轮次的投票其中，quorum即议会系统是每个轮次中实际的参与者，红色标记的是投票了的参与者，voters是quorum的子集显然地，5个投票轮次的编号都不一样，并且议会系统都包含大多数的参与者，保证其交集不会为空，所以编号条件和议会系统条件都是满足的.接下来，我们来具体地分析如何满足特定值条件.