Page 44 - 《软件学报》2021年第6期

1618 Journal of Software 软件学报 Vol.32, No.6, June 2021

2.2.2 反向截断事件
前述反向扩展规则能确保 RUnf 的完备性,但无法保证其有限性.为此,下文将给出反向截断事件的识别规
则,据此保证反向展开过程的可终止性.
定义 8(反向截断事件). 事件 e 为反向截断事件,当且仅当 RUnf 中存在事件 e′,满足以下两个条件.
(1) Mark([e′])≤Mark([e]);
(2) [e′]≺[e].
其中,≺是定义在配置上的偏序,称为 adequate order,满足以下 3 个条件.
(1) ≺是良基的;
(2) ≺是⊂的精炼,Cfg 1 ⊂Cfg 2 意味着 Cfg 1 ≺Cfg 2 ;
(3) 若 Mark(Cfg 1 )≤Mark(Cfg 2 ),Cfg 1 ≺Cfg 2 ,则对 Cfg 2 的任意前缀 E 2 ,有 E 1 满足 Mark(Cfg 1 ⊕E 1 )≤
Mark(Cfg 2 ⊕E 2 ),且 Cfg 1 ⊕E 1 ≺Cfg 2 ⊕E 2 .其中:对于一个配置 Cfg,Cfg⊕E 表示存在事件集 E,使得 Cfg∩E=
∅,且 Cfg∪E 也是一个配置.E 也叫作 Cfg 的前缀.
本文使用≺ r 作为 adequate order,相关证明可参考附录 A 中的定理 1.Cfg 1 ≺ r Cfg 2 定义为:
(1) |Cfg 1 |<|Cfg 2 |;
(2) |Cfg 1 |=|Cfg 2 |∧Lex(μ(Cfg 1 ))<Lex(μ(Cfg 2 )).其中,μ(Cfg)是配置 Cfg 2 映射到Σ上的变迁集合,这个变迁集合
是一个多重集.Lex(μ(Cfg))将μ(Cfg)中的变迁按照 ID 从小到大排序.可以理解为:当两个配置大小相同
时,比较其对应的变迁集合的字典序.
图 5 中的事件 e3 将因事件 e1 而截断,如图 6 所示.这是因为|[e1]|<|[e3]|,即[e1]≺ r [e3],且:
Mark([e1])={p4,p7}≤{p1,p4,p7}=Mark([e3]).
反向扩展和反向截断事件保证了 RUnf 的完备性与有限性,相关证明见附录 A 中的定理 2 与定理 3.
2.2.3 反向展开的可覆盖性判定
本文只考虑安全 Petri 网,可以在 Petri 网上添加源库所 ps、源变迁 ts、流关系(ps,ts),并对∀p∈M 0 添加流关
系(ts,p),从而将求解 M 0 M f 转化为求解{p s } M f .这样仅需判断 RUnf 中是否存在一个配置 Cfg,使得 Mark(Cfg)=
{ps},即可验证 M f 的可覆盖性.以图 4 中的 Petri 网为例,添加源节点后的 Petri 网如图 7 所示.

Fig.6 Event e3 is cut off by event e1 Fig.7 Petri net after adding source nodes
图 6 事件 e3 因事件 e1 而截断 图 7 添加源节点后的 Petri 网

2.2.4 反向展开算法与可覆盖性判定实例
反向展开可覆盖性判定的流程可以总结为:初始时,RUnf 中只有与 M f 相对应的条件集合 CM f ,算法会基于
CM f 计算初始扩展集 Rext.随后,只要 RExt 不为空,则算法将持续进行反向扩展.每次扩展都会从 RExt 中随机取