Page 24 - 《软件学报》2021年第10期

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

在简单的图形化表示方法之外,Petri 网还具有严格的数学定义、执行语义和用于分析的数学理论,提供了丰富
的模型分析工具.文献[21]是 Petri 网领域研究的综述,是 Petri 网理论发展中的一次重要总结.
Petri 网的正则定义如下.
Petri 网(Petri net,简称 PN)是一个五元组 PN=(P,T,F,W,M 0 ),其中,P={p 1 ,p 2 ,…,p m }表示库所(place)的有限集
合,库所中包含若干令牌,作为资源对象;T={t 1 ,t 2 ,…,t n }表示变迁(transition)的有限集合;F(PT)(TP)表示弧
(arc)的集合;W:F{1,2,3,…}表示权重函数;M 0 :P{0,1,2,…}表示初始标记.PT=并且 PT.
Petri 网的发射规则定义如下.
(1) 对一个变迁 t 来说,当且仅当每个输入库所 p,都标记了最少 w(p,t)个令牌,这个变迁才是使能的.其中,
w(p,t)表示由 p 指向 t 的弧的权重;
(2) 使能的变迁可以发射(fire)或不发射;
(3) 当发射一个使能的变迁 t 时,从 t 的每个输入库所 p 中删除 w(p,t)个令牌,在 t 的每个输出库所 p 中添
加 w(t,p)个令牌.其中,w(t,p)表示由 t 指向 p 的弧的权重.
图 1 所示为 Petri 网发射规则的示意图,输入库所的弧权重分别是 2 和 1,输出库所的弧权重为 2,发射导致
变迁的输入库所分别减少两个和一个令牌,输出库所增加两个令牌.

Fig.1 An example of firing an action
图 1 Petri 网发射规则示意

1.4 着色Petri网概述
Petri 网虽然提供了简单的建模元素,但其表达能力较低.为了进一步提高 Petri 网的建模效率,学界提出了多
种高级 Petri 网模型,包括随机 Petri 网(stochastic Petri net,简称 SPN) [22] 、着色 Petri 网(colored Petri net,简称
CPN) [7,23] 等.
着色 Petri 网在 Petri 网模型的基础上添加了颜色集、颜色函数、弧表达式函数、守护函数和初始化函数
等元素.在围绕令牌着色提出一系列改动之后,模型的表达能力得到了很大程度的扩展:令牌通过着色,可以表
达更丰富的语义信息;弧表达式函数对令牌进行选择;另外,还有变迁守护函数对发射条件的控制,使模型的流
程控制能力更强,可以实现复杂的分支选择和控制逻辑.因为着色 Petri 网与 Petri 网相比具有更强的表达能力,
所以在对同一个系统进行建模时,着色 Petri 网能够以相对更少的模型元素进行相同语义的建模.在本文中,我们
使用着色 Petri 网对系统进行建模.
1.5 CPN Tools概述

CPN Tools [24] 是一套着色 Petri 网的编辑、仿真和分析工具,从 2000 年到 2010 年,由丹麦奥胡斯大学(Aarhus
University)的 CPN 组负责研发.2010 年,该工具转交荷兰埃因霍温科技大学的 AIS 组继续开发和维护.CPN Tools
的主要功能包括:(1) 提供了着色 Petri 网的图形化建模工具,能够方便、快捷地建立模型;(2) 提供了着色 Petri
网模型的分析引擎,支持模型仿真、监控和状态空间分析等多种分析工具.
CPN Tools 采用 ML 语言(ML language) [25] 作为模型的定义语言,ML 语言由爱丁堡大学的 Milner 提出,是一
种函数式编程语言.本文使用 ML 语言进行系统建模及一致性检查.由于 CPN Tools 对 Petri 网的符号作了进一
步的修改,以增强表达能力和可视化效果,如在库所中嵌入文字以及双线椭圆来代表折叠的 Petri 网等,因此包含
了不同于标准 Petri 网的符号.为了能够更好地对系统行为加以介绍,本文使用 CPN Tools 中的模型图进行解释
说明.