Page 36 - 《软件学报》2021年第10期
P. 36

3008                                 Journal of Software  软件学报 Vol.32, No.10, October 2021

                 引用采用“页名库所名或变迁名”的格式(在 CPN Tools 中,本文各模型图中的双线矩形内的文字即为页名).状态
                 图中没有输入弧的节点称为初始状态,图中左上角的状态 1 即为初始状态.没有输出弧的节点称为终结状态,图
                 中左下角的状态 2 即为终结状态.可以查看每个状态中各个库所的令牌,并可用来进行系统分析.如图中状态 2
                 仅库所 P3 中有 1 个令牌,其他库所中无令牌.




























                                             Fig.16    An example of state space graph
                                                   图 16   状态空间图样例

                    因为示例网络较为简单,因此可以画出完整的状态空间图.但是,对于复杂模型,可能会有成千上万个状态
                 空间节点,全部画出就变得不可行.但是,CPN Tools 提供了状态空间的查询功能,可以通过 ML 语言编写检查规
                 则,并在计算状态空间时自动检查满足规则要求的状态节点.

                 4.2   实验设置
                    初始状态为 1 个客户端向 3 个数据节点写入副本数为 2 的 1 个文件,文件包含 1 个大小为 64MB 的文件块.
                 无错情况下,模型中的出错标记设置为假;有错情况下,模型中的出错标记变量设为真.分别进行了数据层无错、
                 有错和操作层无错、有错情况下的一致性实验.

                 4.3   数据层一致性分析
                    给定系统约定的副本数,系统满足数据层一致性,当且仅当在任意状态下,一个文件块要么不出现,要么出
                 现的次数为副本数.因此,在这一实验中,不一致状态节点的检查规则为:如果出现了一个文件块,但是出现的次
                 数不等于副本数,则标记为不一致状态节点.
                 4.3.1    无错情况下的数据层一致性
                    无错情况下的数据层一致性实验中的状态空间报告见表 1.
                                   Table 1    State space report of data layer consistency without error
                                          表 1   无错情况下数据层一致性状态空间报告
                                                统计项                          个数
                                                状态节点                          49
                                                终结状态                          9
                                               不一致状态                          2
   31   32   33   34   35   36   37   38   39   40   41