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

郝宗寅 等:Petri 网的反向展开及其在程序数据竞争检测的应用 1619

•
出一个 rext=(t,C),并在 RUnf 中创建相应的事件 e=(t,C).若 e 不为反向截断事件,则对 t 中的每个库所 p 在 RUnf
中创建相关的条件 c=(p,e).之后,通过计算 RExt=RExt∪NE(RUnf,e)更新 RExt.若存在一个事件 e,使得 Mark([e])=
{ps},则说明 M f 可覆盖,终止算法.若最终 RExt 为空,且没有事件 e 满足 Mark([e])={ps},则说明 M f 不可覆盖.反向
展开算法的伪代码如下.
Petri 网的反向展开与目标标识可覆盖性判定算法.
Input: A net system Σ=(P,T,F,{p s }), with target M f ={p 1 ,p 2 ,…,p n };
Output: The coverability of M f .
RUnf={(p 1 ,∅),(p 2 ,∅),…,(p n ,∅)}
RExt=NE(RUnf,∅)
while RExt≠∅ do
poll an extension rext=(t,C) from RExt randomly
create an event e=(t,C) in RUnf
if e is not a reverse cut-off event then
•
for ∀p∈ t, append a condition c=(p,e) to RUnf
if Mark([e])={ps} then
return true
endif
RExt=RExt∪NE(RUnf,e)
endif
endwhile
return false
下面结合图 7 的 Petri 网实例,展示反向展开判定目标标识{p6,p7}可覆盖性的完整流程,见表 1.

Table 1 Example of reverse unfolding
表 1 反向展开实例分析
反向展开流程 RExt RUnf
{rext1=(t3,{c1}),
setp 0. 初始 RUnf 中只有条件 c1,c2. rext2=(t4,{c2})}
step 1. 选择 rext1 进行扩展,在 RUnf 中创建 {rext2=(t4,{c2}),
rext3=(t1,{c3})}
事件 e1=(t3,{c1})及其前驱条件{c3}. {rext2=(t4,{c2}),
step 2. 选择 rext3 进行扩展,在 RUnf 中创建事件 e2=(t1,{c3})及其 rext4=(ts,{c4}),
前驱条件{c4,c5},生成新扩展(ts,{c4}),(t3,{c5}),(t4,{c5}), rext5=(t3,{c5}),
(t4,{c2,c5}).由 RExt 的限制条件删除扩展(t4,{c5}). rext6=(t4,{c2,c5})}
step 3. 选择 rext4 进行扩展,在 RUnf 中创建事件 e3=(ts,{c4}) {rext2=(t4,{c2}),
及其前驱条件{c6},此时已经没有新的扩展. rext5=(t3,{c5}),
step 4. 选择 rext5 进行扩展,在 RUnf 中创建事件 e4=(t3,{c5}),由 rext6=(t4,{c2,c5})}
{rext2=(t4,{c2}),
反向截断事件的定义,e4 会因 e1 而截断,此次扩展中断. rext6=(t4,{c2,c5})}
step 5. 选择 rext6 进行扩展,在 RUnf 中创建 {rext2=(t4,{c2}),
事件 e5=(t4,{c2,c5})及其前驱条件{c7}. rext7=(t2,{c7})}
step 6. 选择 rext7 进行扩展,在 RUnf 中创建事件 e6=(t2,{c7})及其 {rext2=(t4,{c2}),
前驱条件{c8,c9},生成新扩展(ts,{c8}),(ts,{c9}),(ts,{c8,c9}), rext8=(ts,{c4,c8,c9}),
(ts,{c4,c8}),(ts,{c4,c9}),(ts,{c4,c8,c9}),(t3,{c8}),(t4,{c8}),由 rext9=(t3,{c8}),
RExt 的限制条件只保留(ts,{c4,c8,c9}),(t3,{c8}),(t4,{c8}). rext10=(t4,{c8})}
step 7. 选择 rext8 进行扩展,在 RUnf 中创建事件 e7=(ts,{c4,c8,c9})
及其前驱条件{c10},此时目标标识可覆盖,算法结束.

以上就是整个反向展开算法的流程,然而算法目前并没有规定扩展顺序,仅采用随机扩展.实际上,扩展顺
序对反向展开算法的效率有着决定性的影响.接下来将使用启发式技术对反向展开做优化.