B4.17.5State Transition Model设计研究
不可达状态与无出口状态是可由模型机械检出的缺陷
别名: 不可达状态 · 死状态 · 无出口状态
概念解释
在状态转换模型上，有两类缺陷不需要理解设计意图就能查出：不可达状态——建模声称存在的界面情形但从初始状态永远走不到；无出口状态——进入后没有任何转换能带用户离开（或离开路径依赖被忽略的条件）。图算法可以直接把它们算出来。
机制
不可达性由图遍历判定：从初始状态做可达性分析，未覆盖的状态即不可达；无出口性是对每个状态检查出边集合，空集或只指向自身而无用户可触发外向边的闭环即死端。这类检查的价值在于把「用户会被困住吗」「这个界面情形真的存在吗」从人工审查题变成可重复的计算。
怎么研究
该性质来自形式化验证中的可达性分析（reachability analysis）与活性检查（liveness）。研究与实践关注模型忠实度：检出的「缺陷」有多少是实现与模型不一致造成的假阳性，抽象掉的维度（时间、网络失败）会不会正是出口路径缺失的原因。工具化做法是从实现代码提取状态机再分析，减少手工模型的偏差。
边界
机械检查只保证模型内部的结论：模型漏掉的条件（权限、网络、时间）会让「有出口」的判断失真，「不可达」也可能只是模型未画出入口。检出后仍需人工确认是设计冗余、文档过期还是真缺陷。它覆盖不了结果正确性——能到达且能离开的状态里发生什么，状态图本身不回答。
怎么落地
- 关键流程的状态机每次合入前跑可达性与出口检查，把两项检查纳入持续集成。
- 检出的不可达状态逐条处置：删除死代码、补入口，或在模型中说明保留理由。
- 对无出口状态检查超时、取消与返回路径是否存在；缺失即按缺陷修复。
- 用实现提取的模型复核手绘模型，差异清单交给设计与工程共同确认。