Petri 网的虹吸与陷阱

虹吸的空状态形成自锁：要把第一个 token 放回来，操作本身已经要求里面有 token，因此永远无法启动。陷阱则相反，任何可能拿走最后一个 token 的操作，都必须往集合里放回一些东西。

中文名称容易让人把“陷阱”理解成永远死锁。这里它只保证集合总有 token，里面的变迁仍然可能继续工作，其他库所也可能死锁。

逐个变迁核验，不看图猜方向 ​

取库所 $p,q,r$，变迁 $a:p\to q$、$b:q\to p$、$c:q\to r$。令 $S=\{p,q\}$，则

所以 $S$ 是虹吸，不是陷阱。从 $(p,q,r)=(0,1,0)$ 触发 $c$ 后成为 $(0,0,1)$，$S$ 变空，之后 $a,b,c$ 都不能向其重新注入 token。

集合 $T=\{r\}$ 则有 $T\bullet =\varnothing \subseteq \{c\}=\bullet T$，因此是陷阱。一旦 $r$ 收到 token，没有变迁能拿走它；但初态 $T$ 为空并不妨碍以后变为非空，陷阱只保持“有标记”，不保持“为空”。

一步证明足以归纳全部执行 ​

若虹吸 $S$ 当前为空，任何在 $\bullet S$ 中的变迁也属于 $S\bullet$，必须消费 $S$ 中的 token，故不能使能；不在 $\bullet S$ 的变迁不会增加 $S$ 的 token。因此下一步仍空，沿执行归纳即可。

若陷阱 $T$ 当前非空，一步若不消费其中 token，则保持非空；若消费，则对应变迁属于 $T\bullet \subseteq \bullet T$，会输出至少一个 token 到 $T$，所以仍非空。弧权可以大于一，此证明只使用正输出存在；它并不保证总数不下降。

陷阱不等于守恒量 ​

单库所网的变迁 $p\to 2p$ 使 $\{p\}$ 同时为虹吸和陷阱。初态一个 token 后数量依次为 $1,2,3,\dots$，明显不守恒。结构条件保持的是空/非空断言，不是 $y^{T}M$ 的精确数值。

相反，某个线性守恒量可能横跨多个库所并带不同权重，不能直接把其支撑集合与任意虹吸或陷阱等同。二者提供互补的不可达证据。

若初态某虹吸为空，而目标要求其中有 token，则目标不可达；若初态某陷阱被标记，而目标把它全部清空，也不可达。检查一组指定库所是否满足包含关系，只需扫描其相关弧，因而很便宜。

枚举所有极小虹吸或陷阱可能有指数输出规模，不能从单个集合易检查推出全部结构易枚举。即使没有发现上述阻碍，也不能宣布目标可达；这些都是必要条件筛查。

在资源协议中，空虹吸常解释一组资源如何永久耗尽；被标记陷阱常给出“至少保有一份资源”的归纳不变量公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。。是否足以证明全网无死锁，还取决于额外结构，不能对任意加权网无条件推广。