【CPN 学习笔记（三）】—— Chap3 CPN ML 编程语言上半部分 3.1 ~ 3.3

张

张建站

2026/4/8 20:41:08

10分钟阅读

【CPN 学习笔记三】—— Chap3 CPN ML 编程语言上半部分 §3.1 ~ §3.3教材《Coloured Petri Nets》Jensen Kristensen, Springer 2009本篇覆盖§3.1 函数式编程 · §3.2 颜色集构造器 · §3.3 表达式与类型推断一、章节概述第三章介绍CPN ML 编程语言——在 CPN 模型中定义颜色集、声明变量、编写弧表达式和守卫的语言基础。章节内容本篇§3.1函数式编程思想✅§3.2颜色集构造器✅§3.3表达式与类型推断✅§3.4函数定义与多态下篇§3.5递归与列表操作下篇§3.6模式匹配下篇§3.7启用绑定元素的计算下篇二、§3.1 函数式编程2.1 CPN ML 的来历CPN ML 基于函数式编程语言Standard MLSML在其基础上扩展了颜色集和多重集的支持。CPN Tools 使用的是 SML/NJ 实现。选择 SML 的原因CP-net 的数学定义中本身就用到了类型、变量、绑定、表达式求值等概念这些与函数式语言的基础天然吻合。ML 是什么意思ML 全称是Meta Language元语言。1970年代爱丁堡大学的研究人员在开发一个定理证明系统LCF需要一种语言来描述证明策略——也就是用来写操控其他语言的语言所以叫元语言。后来这个语言本身发展成了一门独立的编程语言叫ML。Standard MLSML是它的标准化版本CPN ML 就是在 SML 基础上加了颜色集和多重集的扩展。所以 CPN ML Coloured Petri Net Meta Language名字里的 ML 就是这个历史来源跟机器学习Machine Learning没有任何关系。2.2 函数式 vs 命令式核心差别维度命令式Python / Java函数式CPN ML / SML计算方式执行赋值语句修改内存对表达式求值不修改状态迭代for 循环 / while 循环递归函数变量可以被反复赋值一旦绑定值不可改变函数地位函数是特殊构造函数是一等公民可以传递类型检查运行时Python或编译时Java编译时推断强类型Python 类比CPN ML 中的变量绑定更像 Python lambda 表达式的参数——绑定之后不能改变函数根据输入计算出新值而不是「改变」旧值。在 CPN 模型里变迁发生时将弧表达式中的变量绑定到 token 的颜色值然后对表达式求值——这正是函数式的运作方式。2.3 强类型与类型推断CPN ML 是强类型的每个表达式都有类型类型不匹配在编译时就报错。但通常不需要手动写类型注解——系统会自动推断(* CPN ML 类型推断示例 *) val x 42 (* x : int推断为整数 *) val s hello (* s : string推断为字符串 *) val f fn n n1 (* f : int - int推断为函数 *)Python 对比Python 也推断类型但运行时才检查。CPN ML 在编译时就检查保证仿真不会出现类型错误崩溃。三、§3.2 颜色集Colour Sets3.1 基本类型Basic TypesCPN ML 继承了 Standard ML 的四种基本类型可直接用作颜色集CPN ML 关键字含义Python 类比int所有整数intstring所有文本字符串strbooltrue / falseboolunit只含一个值()None单例colset NO int; (* 序列号颜色集 *) colset DATA string; (* 数据内容颜色集 *) colset BOOL bool; (* 布尔颜色集 *) colset UNIT unit; (* 单元颜色集token 只有一种颜色 () *)unit类型只有一个值()对应 Python 的None。当库所颜色集是UNIT时只需关心「有没有 token」不用关心 token 的具体值。第七章用UNIT限制网络缓冲区容量就是这个用法。3.2 颜色集构造器一览构造器语法作用Python 类比productproduct A * B元组两个或更多类型组合tuplerecordrecord f1:A * f2:B带字段名的结构体dict/dataclassunionunion C1:A C2:B可区分的联合类型Union 枚举标签withwith v1v2v3listlist A同类型元素的有序列表list3.3 product 颜色集元组定义把两个或多个颜色集组合为一个元组。colset NO int; colset DATA string; colset NOxDATA product NO * DATA; (* 数据包序号 × 内容 *) (* 合法的 NOxDATA 值 *) (1, COL) (* 序号1内容COL *) (3, ED ) (* 序号3内容ED *)访问各分量用#1、#2…… 运算符#1 (3, ED ) (* → 3 取第一个分量 *) #2 (3, ED ) (* → ED 取第二个分量 *)Python 对比NOxDATAtuple[int,str]p(3,ED )p[0]# ≈ #1 p → 3p[1]# ≈ #2 p → ED 教材建议product 分量不要超过 4~5 个多了用 record 更清晰。3.4 record 颜色集带字段名的结构定义像 Python 的dataclass每个字段有名字。colset DATAPACK record seq:NO * data:DATA; (* 合法的 DATAPACK 值字段顺序不重要*) {seq1, dataCOL} {dataCOL, seq1} (* 和上面等价 *)访问字段用#字段名运算符#seq {seq1, dataCOL} (* → 1 取 seq 字段 *) #data {seq1, dataCOL} (* → COL 取 data 字段 *)Python 对比fromdataclassesimportdataclassdataclassclassDATAPACK:seq:intdata:strdpDATAPACK(seq1,dataCOL)dp.seq# ≈ #seq dp → 1dp.data# ≈ #data dp → COLproduct vs recordproduct 更简洁record 字段有名字更易读。超过 2 个字段推荐用 record。3.5 union 颜色集可区分联合类型定义把两种不同颜色集合并用构造子标签区分来自哪种颜色集。改进协议中网络上既有数据包DATAPACK也有确认包ACKPACK用 union 统一为一个颜色集 PACKETcolset ACKPACK NO; colset DATAPACK record seq:NO * data:DATA; colset PACKET union Data:DATAPACK Ack:ACKPACK; (* 合法的 PACKET 值 *) Data({seq1, dataCOL}) (* 数据包用 Data 构造子包裹 *) Ack(2) (* 确认包用 Ack 构造子包裹 *)使用case表达式区分处理case p of Data({seqn, datad}) (* 处理数据包 *) | Ack(k) (* 处理确认包 *)Python 对比fromtypingimportUnionfromdataclassesimportdataclassdataclassclassDataPacket:seq:intdata:strPACKETUnion[DataPacket,int]# int 代表 ACK 序号# 使用时需判断类型Python 3.10 matchmatchp:caseDataPacket(seqn,datad):...caseint(k):...⚠️ 注意DATA颜色集名和Data构造子名大小写不同——CPN ML 是大小写敏感的。3.6 enumeration 颜色集枚举定义用with关键字列举所有值值只有名字没有附带数据。colset RESULT with success | failure | duplicate; (* RESULT 只有三种值success、failure、duplicate *)应用示例——表示数据包传输的三种结果case res of success 1pack (* 成功传一个 token *) | duplicate 2pack (* 复制传两个 token *) | failure empty (* 丢包不传 *)Python 对比fromenumimportEnumclassRESULT(Enum):success1failure2duplicate33.7 list 颜色集列表定义用list关键字定义某个颜色集的列表类型。colset DATAPACKS list NOxDATA; (* 数据包的列表 *) colset ACKPACKS list NO; (* 确认序号的列表 *) (* 合法的 DATAPACKS 值 *) [] (* 空列表 *) [(1,COL), (1,COL), (2,OUR)] (* 三元素列表 *)两个重要的列表操作符(* ^^ 是列表连接append*) [(1,COL)] ^^ [(2,OUR)] (* → [(1,COL),(2,OUR)] *) (* :: 是列表构造cons把元素加到列表头部*) (1,COL) :: [(2,OUR)] (* → [(1,COL),(2,OUR)] *) (* 在弧表达式中用 :: 「拆解」列表*) (* 弧表达式 p::rest 会把列表的第一个元素绑定到 p剩余部分绑定到 rest *)Python 对比DATAPACKSlist[tuple[int,str]]# ^^ ≈ list1 list2 Python 列表拼接# :: ≈ [head] rest Python 列表前插用途在库所上放一个「列表 token」实现队列FIFO——新元素用^^追加到末尾旧元素用::从头部取出保证先进先出数据包不会「超车」。列表 token 实现队列^^和::怎么配合先说清楚为什么需要这个。第二章的协议库所 A 上每个数据包是独立的 tokenA 上有 3 个 token (1,COL) (1,COL) ← 重传的 (2,OUR)这时候TransmitPacket可以任意选一个来传于是(2,OUR)完全可能比两个(1,COL)先传出去——数据包发生了超车顺序乱了。解决方案把库所 A 上的多个 token 合并成一个列表 token强制按顺序处理A 上只有 1 个 token [(1,COL), (1,COL), (2,OUR)] ↑ 队列头先进先出现在看^^和::分别怎么用^^负责入队加到尾部SendPacket发送新数据包时把它追加到列表末尾sml(* 弧表达式 *) datapacks ^^ [(n,d)] (* 假设 datapacks [(1,COL),(1,COL)] *) (* (n,d) (2,OUR) *) (* 结果 → [(1,COL),(1,COL),(2,OUR)] *)Python 等价pythondatapacks[(n,d)]# 列表拼接新元素加到末尾::负责出队从头部取TransmitPacket传输数据包时弧表达式写p::datapacks1这不是在构造列表而是在模式匹配拆解列表sml(* 弧表达式 p::datapacks1 出现在「输入弧」上 *) (* 含义从库所 A 的列表 token 里把第一个元素绑定到 p剩余部分绑定到 datapacks1 *) (* 假设库所 A 上的 token 是 [(1,COL),(1,COL),(2,OUR)] *) (* 匹配后p (1,COL)datapacks1 [(1,COL),(2,OUR)] *)Python 等价pythonp,*datapacks1[(1,COL),(1,COL),(2,OUR)]# p (1,COL)# datapacks1 [(1,COL),(2,OUR)]完整的一次传输过程初始状态库所 A 上的 token [(1,COL), (1,COL), (2,OUR)] TransmitPacket 发生输入弧 p::datapacks1 拆解列表 → p (1,COL) ← 取出队头准备传输 → datapacks1 [(1,COL),(2,OUR)] ← 剩余部分传输成功successtrue → p 被追加到库所 B 的列表末尾 → datapacks1 放回库所 A 传输后库所 A[(1,COL), (2,OUR)] ← 队头已被取走库所 B[(1,COL)] ← 新到达的包每次只能取队头后面的包绝对不会跑到前面——超车问题彻底解决。还有一个细节当库所 A 的列表是空列表[]时p::datapacks1无法匹配因为空列表没有头所以TransmitPacket自动不启用——这就是缓冲区为空时不能传输的自然表达不需要额外的守卫。3.8 颜色集综合示例改进协议完整声明colset NO int; colset DATA string; (* product数据包序号 × 数据 *) colset NOxDATA product NO * DATA; (* record同样是数据包但字段有名字 *) colset DATAPACK record seq:NO * data:DATA; (* 确认包等价于一个序号 *) colset ACKPACK NO; (* union网络上的「统一包类型」*) colset PACKET union Data:DATAPACK Ack:ACKPACK; (* enumeration传输结果的三种情况 *) colset RESULT with success | failure | duplicate; (* list队列式网络缓冲区 *) colset DATAPACKS list NOxDATA; colset ACKPACKS list NO;对应的 Python 等价写法仅帮助理解非 CPN 语法fromtypingimportUnionfromdataclassesimportdataclassfromenumimportEnum NOintDATAstrNOxDATAtuple[int,str]dataclassclassDATAPACK:seq:intdata:strACKPACKint# union用构造子区分两种类型PACKETUnion[DATAPACK,int]# int 代表 Ack 的序号classRESULT(Enum):success1failure2duplicate3DATAPACKSlist[NOxDATA]ACKPACKSlist[int]四、§3.3 表达式与类型推断4.1 弧表达式的类型要求位置类型要求弧表达式每次传一个 token等于所连接库所的颜色集类型弧表达式可传多个 token该颜色集的多重集类型ms初始标记颜色集类型或该颜色集的多重集守卫guardbool类型或bool列表4.2 类型推断实例(* 变量声明 *) var n : NO; var d, data : DATA; var success : BOOL; (* 弧表达式 (n,d) *) (* 因为 n:NOd:DATA推断出 (n,d) 的类型是 NO*DATA NOxDATA ✓ *) (* 弧表达式 1(n,d) *) (* 1(n,d) 是一个多重集类型是 NOxDATA ms ✓ *) (* 常见弧表达式 *) if success then 1(n,d) else empty (* then 分支NOxDATA ms *) (* else 分支any ms空多重集属于任意多重集类型*) (* 整体类型NOxDATA ms ✓ *)⚠️常见错误忘记在 then 分支写 1(* 错误写法 *) if success then (n,d) else empty (* then 分支类型NOxDATA不是多重集*) (* else 分支类型a ms多重集*) (* 两者类型不同 → 编译报错*) (* 正确写法 *) if success then 1(n,d) else empty4.3 if-then-else 和 case 表达式两种条件表达式都可用于弧表达式和守卫中if-then-elseif n k then data ^ d (* ^ 是字符串拼接 *) else data (* 类型推断then/else 分支都是 string DATA ✓ *)case 表达式多分支时更清晰case res of success 1pack | duplicate 2pack | failure empty等价的嵌套 if 写法更难读if res success then 1pack else if res duplicate then 2pack else emptycase 的另一种用法——用来计算系数(case res of success 1 | duplicate 2 | failure 0) pack (* 系数为 0 时等价于 empty不产生 token *)Python 对比case res of ...≈ Python 3.10 的match语句matchres:caseRESULT.success:result1*packcaseRESULT.duplicate:result2*packcaseRESULT.failure:resultempty_multisetcase p of Data(...) | Ack(...)在干什么先从问题根源说起。PACKET union Data:DATAPACK Ack:ACKPACK定义了一个联合类型。这意味着一个PACKET类型的 token可能是数据包也可能是确认包放在同一个库所里你从外面看不出来它到底是哪种。构造子Data(...)和Ack(...)就是给 token 贴的标签区分它的身份Data({seq1, dataCOL}) ← 这是一个数据包标签是 Data Ack(2) ← 这是一个确认包标签是 Ackcase p of ...就是剥开标签同时把里面的内容绑定到变量smlcase p of Data({seqn, datad}) (* 现在 n1, dCOL处理数据包 *) | Ack(k) (* 现在 k2处理确认包 *)用 Python 来理解最直接# CPN ML 的 union 构造子相当于 Python 里用类来包装classData:def__init__(self,seq,data):self.seqseq self.datadataclassAck:def__init__(self,k):self.kk pData(seq1,dataCOL)# 创建一个数据包 token# case p of ... 相当于 Python 的 matchmatchp:caseData(seqn,datad):print(f数据包序号{n}内容{d})# n1, dCOLcaseAck(kk):print(f确认包序号{k})为什么要这样设计因为改进协议里网络的四个库所 A、B、C、D 现在颜色集都是PACKET既放数据包也放确认包。当ReceivePacket变迁从库所 B 取 token 时它需要知道这是数据包还是确认包以及序号是多少、内容是什么。case一次搞定这两件事判断类型解包数据。4.4 类型推断的自底向上过程CPN ML 类型推断从子表达式开始逐步推断完整表达式的类型示例从ReceivePacket到DataReceived的弧表达式if nk then data^d else dataStep 1分析then分支data^d^需要两个 stringdata:DATAstringd:DATAstring→ then 分支类型DATAStep 2分析else分支datadata:DATAstring→ else 分支类型DATAStep 3分析条件nkn:NOintk:NOint要求两边类型相同 ✓ → 条件类型boolStep 4整体类型 →DATA✓与DataReceived库所颜色集匹配 ✓五、上半部分总结章节核心概念关键词§3.1 函数式编程求值表达式而非执行赋值函数是一等公民编译时类型检查表达式、类型推断、强类型§3.2 颜色集product元组、record结构体、union标记联合、with枚举、list列表colset、构造子、^^、::§3.3 类型与表达式弧/守卫/初始标记都有类型约束if-then-else 和 case自底向上推断ms、case、类型一致性截图提示本部分对应教材 Fig 3.1改进协议 CPN 模型含 record 和 union 颜色集Fig 3.2 / 3.3 为 TransmitPacket 的标记 M₁ 和 M₂三种绑定成功/丢包/复制。建议在 CPN Tools 中打开改进协议模型截图插入。下篇预告§3.4 函数定义与多态 · §3.5 递归与列表操作 · §3.6 模式匹配 · §3.7 启用绑定元素的计算