反例与见证轨迹

活性 lasso ​

无限路径无法完整打印。有限状态模型中的活性反例通常表示为 lasso

即有限 stem 加可重复 cycle。若规格为 $G(request\to Fgrant)$，反例须包含一个此后永不兑现的请求。请求可以出现在 stem，也可以出现在 cycle；若请求在 stem，cycle 只需持续保留未兑现义务并永远不出现 grant。

循环首尾状态相同确保它能无限重复；只展示一段很长但不闭合的无响应前缀，仍可能在下一步授权，不能证明 liveness 失败。

带 Büchi 或公平条件时，cycle 还必须满足相应接受集合访问要求。任意图环不一定是合法反例。

一条互斥诊断轨迹 ​

两个进程初始都在 N，错误协议允许分别执行 check-free 后再无原子地写锁。反例可为：

(N,N,free)
--p1:check-free--> (T,N,free)
--p2:check-free--> (T,T,free)
--p1:enter-->      (C,T,p1)
--p2:enter-->      (C,C,p2)

每一步同时展示动作与关键状态变量，末状态满足双临界坏谓词。若只列动作名而隐藏 free 的读取结果，就难以看出竞态；若打印全部堆内存，又可能淹没因果链。

最短反例按转移数最少，不一定最有解释力。工具可做 cone-of-influence、变量切片或 trace minimization，但缩减后仍须保留一条可重放的合法路径。

一份可逐项核验的无限反例证书 ​

复用自动机论模型检查公理库自动机论模型检查Automata-theoretic model checking · Automata-based LTL model checking将系统与否定规格 Büchi 自动机同步取积，并以可达接受环判定 LTL 违反行为。的共享例：系统初态为 $r$，标签为 $L(r)=\{request\}$、$L(w)=\varnothing$、$L(g)=\{grant\}$，系统边为 $r\to w$、$w\to w$、$w\to g$、$g\to r$。规格是 $G(request\to Fgrant)$；否定自动机从 $z$ 开始，在读到无授权的请求时可以转到接受态 $b$，而 $b$ 只允许继续读取无授权字母。

使用“积顶点已经消费当前标签”的约定，证书可以打印为下列有限对象。loopIndex=1 指向零起算的顶点数组中第二个状态，闭环边另列，因而不会把重复展示的循环入口误当成额外状态。

productStates = [(r,b), (w,b)]
loopIndex = 1
stemEdges = [(r,b) -> (w,b)]
loopEdges = [(w,b) -> (w,b)]
automatonInitial = z
systemProjection = [r,w]

核验应从证书本身恢复无限路径，而不是相信搜索器给出的“accepting”字符串：

由此得到积序列 $(r,b)(w,b{)}^{\omega }$，标准自动机运行为 $zbbb\cdots$，系统投影为 $r{w}^{\omega }$。令有限序列 $u=((r,b))$、$v=((w,b))$，则序列记号 $u{v}^{\omega }$ 与上面的路径端点记法表示同一行为；打印 stem 的末端和 loop 的入口时虽然都写 $(w,b)$，二者是同一个拼接位置。

最后直接求值原公式：位置 $0$ 有 request，所有 $j\ge 0$ 都没有 grant，故位置 $0$ 的 $Fgrant$ 为假，全局响应性质失败。request 完全可以只在 stem 中出现；要求循环本身再次含 request 会漏掉这份最短而清楚的反例。

若额外要求 $w\to g$ 的 serve 动作弱公平，这份证书就不能作为公平前提下的性质反例：循环使 serve 始终使能，却从不执行。它仍是无公平限制模型的合法反例，也可以用来说明哪个公平假设排除了它。只有同时通过公平条件核验且违反原规格的证书，才反驳公平模型。

已解核验任务：接受顶点为何不够 ​

共享积图还含初始接受点 $(r,b)$，但它没有返回自己的路径。只提交“初态属于接受集”不能证明无限接受；必须继续给出 $(w,b)$ 的非空接受循环。若从系统删去 $w\to w$，证书的 loop 系统边就不合法，而 $(w,b)$ 的下一步监控又被 grant 杀掉；即使两个接受顶点仍可达，原证书也无法修补成无限运行。

这个小任务区分了三个验证层次：初态正确只证明可以开始，逐边正确只证明已列有限路径可以执行，闭环与接受检查才证明无限重复满足否定规格。把安全坏前缀的检查器直接用于活性，会缺失最后一层。

CTL 见证不总是一条线 ​

$EFp$ 的见证是一条到 $p$ 的路径，$EGp$ 的见证是进入全 $p$ 循环的 lasso。然而 $AG(EFreset)$ 的完整证明要为每个可达状态提供某条恢复分支，天然更像子图或树，而不是单条路径。

同样，反驳 $A[\phi U\psi ]$ 可以用一条坏路径，证明它却要覆盖全部分支。工具输出单条样例成功执行，不能作为全称 CTL 公式的证明证书。

模型诊断不是根因证明 ​

反例证明模型违反规格，并给出一个行为见证。它不自动说明哪一行代码是根因，也不判断规格、环境假设或抽象是否错误。

抽象模型中的路径可能是 spurious：每一步抽象转移都存在，却没有一个一致具体执行实现整条路径。需要可行性检查把抽象状态约束沿路径合取，再决定是报告真实错误还是精化抽象。

反例也可能依赖模型人工边界，例如队列溢出状态。报告必须包含配置、边界与公平假设，否则读者无法判断能否在目标实现中复现。

证书检查接口 ​

可检查的安全路径至少含初态证明、每步转移输入和末端性质求值。SAT-based 工具可附模型赋值，PDR 可附归纳不变式；证明对象越独立，可信计算基越小。

隐私或状态巨大时可以投影输出，但内部验证仍需对完整状态确认合法性。把日志中看似相邻的事件拼成路径，若缺少隐藏状态连续性，不构成形式证书。

同一个性质可能有多条反例，搜索顺序决定首先返回哪条。按长度最短、按输入变化最少、按因果切片最小是不同优化目标，彼此不保证一致。工具若进行 trace reduction，应在缩减后重新执行每个 guard 和 update；仅删除“看起来无关”的步骤可能让后续状态不再可达，得到一份易读却无效的故事。

对于非确定环境，反例中的环境选择是见证的一部分。若部署假设禁止该输入或故障模式，应修改并验证环境模型，而不是从输出中手工删掉该分支。

反例重放还应固定初始状态、随机种子或调度决策；否则同一外部输入在非确定模型中可能走向另一条合法路径。可复现性是诊断质量，不替代原始路径的形式合法性检查。