SMV 与 TLA+ 规格模式

两种状态关系表达 ​

SMV 风格用有限类型变量、初始约束和 next assignment 描述同步转移。例如布尔锁可写成概念形式：

init(lock) := FALSE
next(lock) := case acquire : TRUE; release : FALSE; TRUE : lock; esac

所有 next 表达式共同定义当前—下一状态关系，符号模型检查公理库符号模型检查Symbolic model checking · BDD-based symbolic model checking用布尔公式或 OBDD 整体表示状态集合与转移关系，并通过量化和不动点运算检查时序性质。再以 BDD 或 SAT 操作它。

TLA+ 风格把变量元组记为 $vars$，规格写成

其中 $Next$ 是动作析取，$[Next{]}_{vars}$ 允许 $Next$ 步或所有变量不变的 stuttering step。两者都描述状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。，却对同步更新、停顿和模块接口采用不同表面结构。

原子动作与帧条件 ​

TLA+ 动作是当前与下一状态上的谓词。动作 Acquire(p) 应同时写 guard、更新和未改变变量：

漏写 frame condition 可能让未约束变量在下一状态任意变化。SMV 的 next assignment 若采用默认保持，也必须确认语言/工具的实际规则，不能靠伪代码直觉。

动作原子性来自规格边界。把“检查空闲并写 owner”放在一个 action 中，会排除两个进程同时读空闲的竞态；若实现分成可交错步骤，规格需相应细化或证明 refinement。

请求队列轨迹 ​

状态含 owner 与有限队列 q。Request(p) 把 $p$ 加入队尾，Grant 在 owner 为空且队列非空时弹出队首并赋给 owner，Release(p) 清空 owner。

一条轨迹是

安全不变式可要求 owner 最多一个进程；活性要求每个入队请求最终获 grant，则还需队列公平与调度假设。

仅用有限 SMV 队列可直接穷举；TLA+ 模型也常人为设有限进程与队列界供 TLC 检查。边界内无反例不自动证明无界参数化系统。

SMV 的 synchronous assignment 表面上同时更新全部变量，右侧都读取旧状态。把第二个 next expression 理解成可读取第一个刚更新的值，会把并行赋值错写成顺序赋值。需要顺序微步时，应增加 phase 或 program-counter 变量。

TLA+ action 中所有 primed variables 同样描述一个原子下一状态。动作析取的不同分支若漏 UNCHANGED，未提及变量并不会凭直觉自动保持，完整 action formula 必须约束下一状态。

隐藏与 refinement mapping ​

实现规格可引入缓存、程序计数器等辅助变量。对外行为通过 existential hiding 或 refinement mapping 投影到抽象变量；实现的若干内部步可对应抽象 stuttering。

映射必须让每个实现初态对应抽象初态，每个实现步对应抽象 $Next$ 或 stutter。仅比较两边变量名相同不足以证明 refinement。

若隐藏变量影响未来可见动作，它可以被投影但不能被语义遗忘；映射证明仍需用它解释为什么下一抽象步合法。

history variable 只记录过去，prophecy variable 预测未来选择，可帮助构造 refinement mapping。它们必须是保守扩展：每条原行为能扩展出辅助变量取值，投影后不新增或删除可见行为。随意加入“未来答案”并据此限制当前动作会缩小系统，而非证明原实现。

当一个实现步对应多个抽象步时，简单 stuttering mapping 不够，可能需要加中间抽象状态或改变动作粒度；把一对多映射硬说成一次抽象原子步会漏掉中间可观察行为。

公平性模式 ​

TLA+ 常对 action 写 $W{F}_{vars}(A)$ 或 $S{F}_{vars}(A)$；SMV 工具用 FAIRNESS/justice/compassion 约束可接受路径。时序性质公理库时序逻辑Temporal logic · Temporal modal logic在执行序列上解释下一步、最终、始终与直到，并区分线性时间和分支时间的统一规格层。只在满足这些假设的路径上判断。

给 Grant 加弱公平，只有当它从某时刻起持续使能才保证执行；若其他动作反复让 guard 暂时失效，强公平才可能排除饥饿。公平对象必须是具体 action，而非含多种分支的宽泛 Next。

过强 fairness 能让错误协议“证明”活性。规格应把环境假设、调度假设与系统保证分别列出。

SMV 的 fairness 常作为路径接受约束，TLA+ fairness 是时序公式的一部分。两者翻译时要检查 action enabled 的定义是否排除 stuttering；否则一个始终停顿的路径可能被错误视为执行了公平动作。

对带参数的 action，$WF(Next)$ 与对每个实例 $p$ 分别写 $WF(A(p))$ 强度不同。前者可能只保证某个实例持续推进，不能推出每个请求者都不饥饿。

工具边界 ​

SMV/TLA+ 是规格与工具生态，不是一种共同逻辑的两个语法皮肤。SMV 偏有限变量和时序模型检查，TLA+ 可写无限数学状态但 TLC 仍需有限可枚举实例。

类型正确、模型检查通过和定理证明是不同保证。常量实例、对称集合和状态约束都会改变被检查模型，运行配置应与规格一起版本化。

对称约简常把进程 ID 置换视为等价，但规格若点名某个特殊进程，或公平性按实例施加，置换群便不再保持性质。工具自动 symmetry reduction 前应核对常量、原子命题和 fairness 都在置换下不变。

模型配置还会指定常量替换、state constraint 和 action constraint。constraint 直接删除状态或转移，可能让性质虚假成立；只有它被证明为环境假设或不变量时，结果才可解释。