简介：面向着色Petri网（CPN）初学者的入门指导资料，以CPN Tools为操作环境，系统讲解从基础概念、模型构建到模拟分析与状态空间分析的全流程。压缩包只有1个doc文档，大小约1.3MB，便于本地离线阅读。已有1609人学习下载。文档对CPN中的Places、Transitions、Arcs等核心要素做了通俗解释，并结合GUI界面介绍模型元素构建、层次建模、语法检查、代码生成及图形化反馈；同时覆盖CPN建模语言的网结构、声明与标注、变迁使能与发生、步骤与并发冲突、模块化设计和时间建模等内容。后半部分重点讲解模拟实验、状态空间分析（含完全状态空间、状态空间报告、查询函数）以及性能分析（含赋时模型、性能测量、数据收集和统计输出），帮助零基础读者建立完整知识框架，并理解复杂系统并发、同步和资源竞争行为的建模与优化方法。教程内容结构清晰，适合计算机科学、通信网络、制造系统等领域的初学者查阅。

1. 从通信协议到着色 Petri 网：这份 CPN 教程值不值得从头读

第一次翻开 CPN（Coloured Petri Net，着色 Petri 网）教程，很多人是被左下角那堆colset、val、++劝退的——一眼看上去像编程语言，再一眼又像画图工具。这份教程恰恰选了最不劝退的打开方式：它不要求你先学 Standard ML，而是拿一个"发送器-网络-接收器"的停止等待协议，把建模语言、工具操作、模拟、状态空间分析串成一条线，每一步都能在 CPN Tools 里看到反馈。CPN 把 Petri 网的图形语义和 SML 的类型系统结合起来：库所存令牌，变迁定义规则，令牌带着颜色值，天然覆盖并发、同步和资源竞争。它适合正在用 CPN Tools 做课程设计的新手，也适合想知道 CPN 能不能扛住协议验证、流程分析的工程师。按教程自己写的读者指南，读完前四章就能动手建模型，后面的状态空间、性能分析和可视化按需再补，不用一口气啃完。

2. CPN 建模语言：把库所、颜色集、多重集一次性讲透

这一章是整份教程的地基，也是最容易让新手以为自己在学编程语言的地方。其实 CPN 建模语言只有三个层次：声明段定义类型和数据、网结构定义拓扑、标注定义行为和初始状态。把这三层拆开理解，后面所有操作都是在这个框架里填东西。

2.1 网结构与颜色集：库所、变迁、令牌和多重集

先看图的第一印象。教程里的协议模型由 8 个库所、5 个变迁和若干弧组成，库所画成椭圆，变迁画成矩形，弧只能连接库所和变迁，不允许同类节点直接相连。库所代表系统状态，每个库所里可以有零到多个令牌，每个令牌自带一个数据值，这个值就叫令牌颜色。所有可能颜色的集合由颜色集（colset）定义，用 CPN ML 关键字colset声明，本质上就是类型定义。

colset NO = int; colset DATA = string; colset NOxDATA = product NO * DATA;

这三行声明了三个颜色集：NO是整数，用来建模协议里的序列号；DATA是字符串，用来建模数据包的有效载荷；NOxDATA是前两者的笛卡尔积，也就是"(序列号, 数据)"这样的二元组。定义好颜色集之后，库所下面标注的颜色集名称就决定了这个库所里能放什么类型的令牌。

令牌的存放形式是多重集，这一点很容易被忽略。多重集和普通集合的区别在于，同一个值可以出现多次，1'(1,"COL")表示颜色值为(1,"COL")的令牌出现一次，++是多重集的并运算。教程里用一段val声明定义了初始要发送的 6 个数据包：

val AllPackets = 1'(1,"COL") ++ 1'(2,"OUR") ++ 1'(3,"ED ") ++ 1'(4,"PET") ++ 1'(5,"RI ") ++ 1'(6,"NET");

注意1'这个写法：它左边的数字表示该令牌出现次数，为 1 时可以省略。很多新手在弧表达式里直接写(n,d)而不写1'(n,d)，语法上没问题，但思想上必须清楚——弧表达式求值的结果永远是一个多重集，不是单个值。这个认知差会在第 5 章的排查记录里再次出现。

2.2 弧表达式与变量绑定：使能判定怎么算

光有静态结构不算模型，真正让模型跑起来的是变迁的使能与发生机制。一个变迁要在一个状态下使能，必须存在一个变量绑定，使得每条输入弧上的弧表达式求值后，得到的所有令牌颜色多重集都能从对应库所的当前标记中取出来。

以教程里的SendPacket为例，它连了两条双箭头弧，弧表达式分别是n和(n,d)。这里的n和d是声明过的变量：

var n : NO; var d : DATA;

绑定<n=1, d="COL">对初始状态是成立的，因为NextSend库所里只有颜色为 1 的令牌，PacketsToSend里恰好有(1,"COL")这个令牌。于是SendPacket在初始状态就是唯一使能的变迁，教程里用粗边框把它标了出来。

这里有一个关键规则：同一个变量在一次绑定中只能取一个值。如果n同时出现在两条输入弧上，两条弧上的n必须绑定为同一个值。不少人在设计模型时想让同一个变量从两个库所取不同数据，结果怎么调都使能不了，原因就在这里。正确做法是用两个不同变量，或者在弧表达式里构造一个对偶结构。

变迁还可以挂警卫（guard），本质上是布尔表达式，只有警卫求值为真的绑定才允许发生。教程在 6.1 节才正式引入警卫，但语法上很简单，直接在变迁属性里写：

[n = k]

这条警卫表示只有绑定满足n = k时变迁才使能。对于接收端来说，这就实现了"只接收期望序列号的数据包"的逻辑。警卫是给使能绑定加约束的最直接手段，性能分析模型里几乎每个变迁都要用到。

2.3 步骤、并发与冲突：调度语义的底层逻辑

CPN 的每一步表示一个绑定元素发生：选中一个使能变迁和一组满足条件的变量绑定，从输入库所移除多重集，向输出库所添加多重集。双箭头弧是两条方向相反的弧的缩写，同一变量绑定下从库所取走什么同时加回什么，所以教程里SendPacket发生时PacketsToSend和NextSend的标记不变，相当于允许无限重发。

并发和冲突是建模并发系统时最需要想清楚的点。如果两个变迁都能使能，而且它们的发生互不影响，那它们是并发的，可以任意顺序发生；如果两个变迁共享一个输入库所，而该库所的令牌不足以同时满足两者，就产生冲突，发生一个之后另一个可能就禁用。教程很明确地提醒：冲突不是错误，而是模型要表达的资源竞争语义。

初始状态下唯一使能的是SendPacket，但一旦进入状态 M1，TransmitPacket就有两个绑定使能：success=true和success=false。这两个绑定代表网络传输成功或丢包，是典型的非确定性选择。模拟时由用户手动选或由自动模拟随机选，状态空间分析时则把所有选择都枚举一遍。理解这一步，后面看状态空间报告里的多叉结构就不会慌。

2.4 层次模块与时间建模：向大型模型过渡

单页模型规模一大就不可读，CPN 的模块机制就是为了解决这个问题。教程 2.4 节讲的分层结构机制，允许一个变迁对应一个子页（subpage），子页有自己的库所和变迁，通过端口库所（port）和插槽库所（socket）与父层交换数据。这和编程里的函数抽象是一个思路：对外暴露接口，内部自由实现。做课程设计时，如果导师要求模型必须分层，这一节就是你要反复看的部分。

时间建模是 CPN 相对普通 Petri 网的一大增量。给弧表达式加@+后缀表示相对当前全局时钟的时间延迟，给库所标记加@后缀表示绝对时间戳。一个典型做法是给传输动作加一个随机延迟：

fun TransmitTime () = 1.0;

然后该变迁的输出弧表达式写成：

(n, d) @+ TransmitTime()

这句表示发送动作发生后，令牌在TransmitTime()个时间单位之后才进入输出库所。延迟可以是常量，也可以是服从某种分布的随机函数。模型一旦引入时间，就能做性能分析，但也意味着状态空间会变大，因为时间参与标记构成。教程把这部分放在性能分析章节的入口，说明它是后续 6 章内容的必要准备。

3. CPN Tools 实操：从空画布到第一个协议模型的完整动作

理论部分看完，紧接着就要开软件。CPN Tools 的界面和大多数 Windows 工具完全不一样，没有菜单栏也没有下拉菜单，第一次打开容易不知道点哪。这份教程在 3.1 节花了不少篇幅讲 GUI 设计逻辑，其实核心就一句话：所有操作都在图形上直接完成。

3.1 没有菜单栏的交互：工具面板和标记菜单

CPN Tools 把常用操作放在了建模区边缘的工具面板上，选中工具后点击图形元素就能创建对应对象。另一个高频交互是右键长按弹出标记菜单，增删节点、复制粘贴、修改属性都在这里。教程反复强调"直接操纵"这个词，意思是你看得见的模型就是数据本身，不需要在属性对话框和画布之间来回切换。

第一次上手时我建议只记住三件事：工具面板选库所、变迁、弧；右键长按呼出标记菜单；双击节点进入属性编辑。剩下的帮助和撤销都在标记菜单里能找到。教程 3.5 节提到的图形化反馈很有用——模型元素有问题时，图上会直接画出红框或黄框，鼠标悬停有提示文本，不用等编译报错。

3.2 构建一个最小模型的完整步骤

从零开始建停止等待协议模型，按教程 3.2 节的顺序操作即可。先创建声明段，再拖库所和变迁，最后连弧并填表达式。

1. 在声明编辑器里输入颜色集、常量、变量，也就是 2.1 节那几段colset、val、var。
2. 用工具面板创建 8 个库所，分别命名为PacketsToSend、NextSend、A、B、C、D、NextRec、DataReceived。
3. 双击每个库所，在属性对话框里设置颜色集和初始标记。比如NextSend的颜色集选NO，初始标记写1；DataReceived的颜色集选DATA，初始标记写""。
4. 创建 5 个变迁，连接弧线。弧的表达式直接在弧属性里填n、(n,d)、(n,d)@+...这些 CPN ML 表达式。
5. 给ReceivePacket变迁填写警卫[n = k]。

每完成一步，模型元素旁边的标注都会实时更新。CPN Tools 的增量检查机制会在你每次编辑后立刻做语法和类型检查，有错会在元素上标红。所以建模过程其实是一个"边画边查"的过程，不是等全部画完再统一排错。

3.3 层次模型怎么建：子页、端口和插槽

层次模型是教程 2.4 和 3.3 节一起讲的。在父页选中一个变迁，右键选择创建子页，该变迁就变成一个 substitution transition，双击它进入子页继续细化。子页里的库所需要与父页通信时，把库所属性设为端口库所（port），并指定端口类型；父页对应位置放一个插槽库所（socket），建立端口和插槽的关联。教程里的演示很直观，但实际做的时候有一个点容易漏：端口库所的类型必须和插槽库所的颜色集一致，否则父子页数据交换直接报错。

关于堆叠标记（stack marking），这是调试层次模型时的利器。子页和父页是同一模型的不同视图，同一时刻模型只有一个全局标记，但各层页面可以分别显示自己关心的局部标记。教程提到这个概念是为了解释为什么子页里的库所标记看起来和父页对不上——不是模型错了，是视角不同。

3.4 语法检查和代码生成：把错误留在画布上

CPN Tools 的语法检查是增量且可视化的。声明段每次修改都会被重新编译，库所和变迁的属性每次编辑都会被检查。教程 3.4 节建议的流程是：先检查声明区有没有红色标识，再逐个检查模型元素上的红色边框，最后看 Messages 窗口里列出的错误明细。

代码生成（Generate Code）是模拟前的一个加速步骤，把 CPN 模型编译成可高效执行的代码，适用于后面自动模拟和性能分析。教程特别提醒，代码生成前必须保证模型通过语法检查，否则生成的代码可能是空的或者过时的。我在实际项目中就吃过这个亏：改了模型忘了重新生成代码，跑了半天模拟发现用的还是旧结构。

4. 模拟与状态空间分析：把行为验证变成可复现的证据

教程第 4 章和第 5 章是使用频率最高的部分。模拟负责探索"可能的执行路径"，状态空间分析负责回答"所有可能的执行路径里有没有问题"。两者的关系就像调试器和形式化验证工具的关系，前者帮你找 bug，后者帮你证明没有某类 bug。

4.1 交互式模拟：像单步调试一样观察状态变化

交互式模拟的界面逻辑和调试器几乎一致。进入模拟模式后，画布上会显示当前使能的绑定元素列表，你选择其中一个点击发生，模型状态就前进一步，受影响库所的标记会实时更新。教程用停止等待协议演示了一条完整路径：从初始状态一路经历SendPacket、TransmitPacket、ReceivePacket、TransmitAck、ReceiveAck五个变迁，回到"发送器准备发送下一个包"的状态。

做交互式模拟时有个习惯值得养成：每走一步，先看当前标记下有哪些使能绑定，再想清楚为什么只有这些绑定使能。教程 2.2 节已经讲过使能判定规则，这一步就是把规则可视化。如果某一步出现了预期之外的使能变迁，说明弧表达式或警卫写错了，趁模型还小赶紧改。

4.2 自动模拟与断点：压测前设置好停止条件

自动模拟的目的是尽快跑完大量步骤，用于测试和性能分析。教程指出，测试时通常需要设置断点和停止条件。CPN Tools 的断点本质上是一个标记谓词，比如"当DataReceived里的令牌数达到 6 时暂停"。

这类条件在工具里一般写成基于标记的布尔表达式，例如检查某个库所的当前标记是否满足某个多重集条件。新手容易犯的错误是只设置一个固定步数上限，不设语义上的停止条件，导致模拟跑过头了还在继续发送数据包。正确做法是：先明确这次模拟要验证什么属性，再把该属性翻译成断点条件。验证协议正确性时，最常用的停止条件是"所有数据包都到达且确认全部处理完"。

4.3 完全状态空间：从一条路径到所有路径

状态空间分析把模型所有可达标记作为节点，把绑定元素发生作为弧，构造一张有向图。这张图一生成，很多问题就有确定答案了。教程强调两点：状态空间可以完全自动构造；构造结果可以通过报告和查询函数来解读。

赋时模型也可以做状态空间分析，但时间会作为标记的一部分参与状态比较，这让状态空间比非赋时模型大得多。所以在做验证之前，建议先想清楚这一个问题：我到底要验证功能正确性，还是性能指标？如果只是功能正确性，可以先去掉所有@+延迟，把模型变成非赋时模型再构造状态空间，速度会快很多。性能分析留在模拟阶段做，两者不要混在同一个模型里验证。

4.4 状态空间报告和查询函数：读懂数字背后的含义

状态空间构造完成后，教程 5.3 节列出的报告项目几乎是固定的，读报告是验证的第一步。下面这张表把最关键的几项列出来：

光看报告还不够，教程 5.4 节的查询函数才是定制化验证的入口。最常用的是PredicateNodes，它遍历状态空间，返回满足条件的节点列表。比如要找出所有死锁状态，可以写：

fun DeadMarkingNodes () = PredicateNodes( FullSTATE, fn n => List.null(OutArcs n), NONE);

参数含义：FullSTATE指定用完全状态空间；fn n => ...是谓词函数，List.null (OutArcs n)判断该节点没有出弧，即没有可发生的变迁；NONE表示不限制返回数量。这个函数返回所有死锁标记的列表，配合EvalNode可以查看具体标记内容。查询函数写一次可以反复用，比肉眼翻报告可靠得多。

5. 性能分析与可视化：五个常见坑的排查记录

教程第 6 章和第 7 章分别讲性能分析和可视化，这两部分连着用效果最好：性能分析产出数据，可视化把数据背后的行为展示给不熟悉 CPN 的人。但这一章也是翻车重灾区，我把自己见过的、踩过的五个高频坑按"现象-原因-解决"整理出来。

5.1 把模型变成赋时模型：用 @+ 给动作加延迟

性能分析的前提是模型必须赋时。非赋时模型里时间没有意义，模拟步数再多也测不出吞吐量。标准做法是给关键变迁的输出弧加@+延迟，延迟值可以是常量，也可以是采样自某个分布的随机函数：

fun ServiceTime () = 2.0;

然后在发送变迁的输出弧上写：

(n, d) @+ ServiceTime()

这样每次发送动作发生，令牌要在当前全局时钟基础上加 2 个时间单位后才进入输出库所。测试不同设计方案时，只需替换ServiceTime的函数体，不需要改动网结构。教程 6.6 节提到的模型参数及对比配置，本质就是这个思路。

5.2 数据收集与统计：测延迟、吞吐量和队列长度

CPN ML 支持引用类型，可以在模型里声明数据收集器。我常用的模式是声明一个ref累积量，在变迁发生时更新：

val totalDelay = ref 0.0; fun recordDelay d = totalDelay := !totalDelay + d;

然后在变迁动作里调用recordDelay。模拟结束后，在命令行执行!totalDelay就能拿到累计值，除以发生次数就是平均延迟。教程 6.3 节和 6.4 节讲的统计和输出，核心就这两行。注意引用类型的初始化要在声明段完成，否则每次模拟重置时收集器会残留上一轮数据，导致后续实验的统计结果错乱。

5.3 可视化：用消息序列图给外行讲清楚协议行为

教程第 7 章的交互图形和消息序列图不是给建模者自己看的，而是给项目里不写模型的人看的。消息序列图把每次变迁发生抽象成一条消息线，展示哪些组件在什么时间交换了什么信息。做课程答辩或项目评审时，把 CPN 模型跑一遍再配上消息序列图，比对着网结构讲半天有效得多。

消息序列图在 CPN Tools 里是从模拟轨迹生成的，所以使用前提是先有一段完整的模拟记录。生成后它只是展示层，不会反过来修改模型行为。如果图里的消息顺序不对，回到模型里查，别在可视化工具里找问题。

5.4 五个常踩的坑：现象、原因、解决

坑一：弧表达式类型不匹配，变迁永远不使能。现象是变迁状态始终显示禁用，检查绑定列表为空，弧表达式看着也对。原因大多是弧表达式求值结果不是多重集，或者变量类型和库所颜色集不一致。解决方法是把弧表达式写成显式多重集形式，比如1'(n,d)，并确认n、d的类型声明分别匹配库所颜色集的组件类型。

坑二：同一个变量想绑两个不同的值。现象是设计意图是"从库所 A 取 x，同时从库所 B 取另一个值"，结果绑定不存在。原因是同一个变量在一次绑定中只能取一个值，两条输入弧同时引用它，要求的是同一个值。解决方法是把变量拆成两个不同名字，或者在建模时就意识到该用NOxDATA这样的组合颜色集。

坑三：初始标记改了，当前标记没重置。现象是模拟起点和自己设想的状态不一致，模型行为看起来"很随机"。原因是当前标记和初始标记是两回事，修改了初始标记定义后，当前标记不会自动同步。解决方法是在开始新一轮模拟前显式重置模型到初始状态，把模拟模式切回初始标记再执行。

坑四：序列号无限递增，int 类型溢出。现象是长时间自动模拟后，序列号令牌出现异常值或状态空间分析报错。教程里明确提过，CPN Tools 的int类型是 31 位有符号整数，k+1这种无限递增早晚会撞到边界。解决方法是做取模运算，或者根据协议窗口大小限定序列号范围。模拟之前先估算最大可能值，是省内存也是省事故。

坑五：状态空间爆炸，生成过程停不下来。现象是点击构造完全状态空间后，进度条一直跑，节点数指数增长，最后内存耗尽。原因是模型本身无界，比如库所里令牌可以无限堆积。解决方法是先用自动模拟探查规模，然后对模型做抽象：合并无关令牌、用颜色集压缩对称状态、引入层次模块限制局部状态，或者改用 SCC 状态空间只保存强连通分量。

6. 用状态空间查询函数定位死锁：一个可以直接抄的技巧

最后落在一个具体的验证技巧上：把 4.4 节那个查询函数变成工作流的一部分。我现在的习惯是每建完一个模型，不管模拟跑得多顺，都强制走一遍"查询死锁 + 查 SCC + 读报告"三件套。

第一步，用PredicateNodes找出所有死标记节点。如果死标记数量大于预期，逐个用EvalNode展开，看是协议正常结束还是意外卡死。停止等待协议里，正常结束状态是"所有包都已确认"，这个状态没有出弧，但它不是死锁。区分这两者的办法是检查死标记里库所的令牌内容，而不仅仅是数量。

第二步，读 SCC 报告。如果存在非平凡的强连通分量，说明模型有循环行为。协议模型有循环是正常的（重传循环），但业务模型里出现不明循环往往意味着活锁。教程 5.3 节的状态空间报告里会单独列出 SCC 统计，这一项值得每次都看一眼。

第三步，把查询结果和模拟轨迹对照。查询函数给出的是静态结论，模拟轨迹展示的是动态路径。两者结合，既能回答"有没有死锁"，也能回答"死锁是怎么到达的"。

有一次我做一个某跨平台系统的流程验证，状态空间报告显示有两个死标记，模拟怎么跑都正常，我一度以为报告算错了。后来用EvalNode展开才发现，是某个分支的卫士条件写反了，只有在特定消息序列下才会走到那个状态——模拟时压根没随机出那条路径。从那以后，我每次建模都强制走一遍查询三件套，模拟只是辅助手段，状态空间才是最终裁判。希望这个习惯对你也有用。

下载这份教程，照着第 3 章把停止等待协议模型建出来，再用第 5 章的方法跑一遍状态空间报告，你会比我更快体会到形式化建模的确定性。祝建模顺利。

本文还有配套的精品资源，点击获取