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

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

与 e2 反向冲突;
(3) 反向并发:若¬(x 1 ≤x 2 ∨x 2 ≤x 1 ∨x 1 #x 2 ),则称 x 1 与 x 2 反向并发,记为 x 1 ||x 2 .图 3(b)中,c3 与 c4 反向并发.
RON 满足以下 3 个性质.
•
(1) ∀c∈C:|c |≤1;
(2) RON 中没有反向自我冲突,即:不存在事件 e∈E,使得 e#e;
(3) F′是无环的,即 F′的反自反传递闭包是一个偏序.
定义 2(反向配置). RON 中的反向配置 Cfg 为若干个事件的集合,满足以下两个性质.
(1) 若事件 e∈Cfg,则∀e′<e:e′∈Cfg;
(2) Cfg 中不存在反向冲突的事件,即∀e,e′∈Cfg:¬(e#e′).
定义 3(反向局部配置). 特别地,将{e′|e′∈E∧e′<e}定义为事件 e 的反向局部配置,记作[e].
图 3(b)中,[e1]={e1},[e3]={e2,e3}.
•
•
定义 4(反向切). 对于配置 Cfg,定义其反向切为 Cut(Cfg)=(CM f ∪ Cfg)\Cfg .另外,对于一个条件集合,若其各
元素之间两两反向并发,则称其为一个 co-set.不难发现,Cut(Cfg)是一个 co-set.
图 3(b)中,Cut([e2])={c3,c4},Cut([e3])={c5}.
反向配置、反向切会在第 2.1.3 节中用于建立反向出现网标识与 Petri 网标识间的映射关系.
2.1.3 反向展开
对于给定的 Petri 网Σ=(P,T,F,M 0 ),需验证目标标识 M f 的可覆盖性.定义Σ和 RON=(C,E,F′,CM f )各节点间的
映射关系μ:C∪E→P∪T 如下.
(1) 若 c∈C,则μ(c)∈P;若 e∈E,则μ(e)∈T;
•
•
•
•
(2) ∀e∈E, e 到 μ(e)在μ的约束下满足双射关系,e 到μ(e) 在μ的约束下满足单射关系.这里与正向展开不
•
•
同,在反向展开中,e 到μ(e) 可以不满足满射关系;
(3) CM f 与 M f 在μ的约束下满足双射关系.
定义 5(反向标识). 定义 Mark(Cfg)=μ(Cut(Cfg))为配置 Cfg 的反向标识.Mark(Cfg)可看作 RON 的一个中间
标识,M f 的可覆盖性判定可转化为 Mark(Cfg)的可覆盖性判定 [19] .
图 3(b)中,Mark([e2])=μ({c3,c4})={p2,p3},Mark([e3])=μ({c5})={p1}.
定义 6(反向展开). 在上述概念的基础上,Petri 网Σ中目标标识 M f 的反向展开定义为一个二元组 RUnf(RON,
μ),满足以下性质:
(1) RUnf 是完备的:记Σ的初始标识 M 0 ,若 M 0 M f ,则在 RUnf 存在一个反向配置 Cfg,使得 Mark(Cfg)⊆M 0 .
这里只需要保证 M f 的可覆盖性不被破坏即可,不必获取全部触发序列;
(2) RUnf 是有限的,即 RUnf 中包含有限的条件与事件.

2.2 反向展开算法
给定 Petri 网Σ=(P,T,F,M 0 )和需要进行可覆盖性判定的目标标识 M f ,反向展开算法的基本思想如下:首先,针
对 M f 中每个库所,在 RUnf 中添加一个相应的条件,即创建 CM f ;之后,从 CM f 出发逐步反向扩展,添加能生成这些
条件的事件以及这些事件使能所需的条件,并对冗余的事件进行截断.如此重复,直到一个反向标识能被Σ的初
始标识所覆盖,或者能证明目标标识不可覆盖.
接下来将结合图 4 所示的实例,给出反向扩展与反向截断事件的准确定义,并介绍目标标识可覆盖性的判
定方法.假设图 4 中需进行可覆盖性判定的目标标识为{p6,p7}.
2.2.1 反向扩展
•
定义 7(反向扩展). 反向扩展为一个二元组 rext=(t,C),其中,C 是一个 co-set,μ(C)⊆t ,记反向扩展组成的集合
为 RExt.
对每一个从 RExt 中选中并用以扩充 RUnf 的反向扩展 rext=(t,C)而言,一方面需要向 RUnf 中添加一个事件
•
e=(t,C);同时,需要为 t 中的每个库所添加一个条件至 RUnf 中.之后重新计算 RExt,记此过程为 NE(RUnf,e).