如何诊断TLA+模型中的不可达代码问题？

1. 利用TLC覆盖率分析定位未触发转移 #

• 打开TLC模型检查器的Coverage标签页，完成验证后，它会列出所有PlusCal生成的TLA+动作，从未执行的动作会被明确标记。你标注<== dead的行对应的动作会显示为未覆盖，同时能直接看到其触发条件（v1=2）从未满足。
• 勾选「Show Coverage in Spec」选项，可直接在原代码中高亮未覆盖部分，直观定位死代码位置。

2. 添加死动作可达性断言强制检测 #

若想让TLC主动识别某个动作无法触发的问题，可手动添加断言：

AssertDeadAction == <> [ActionThatNeverFires]_vars

将ActionThatNeverFires替换为你标记<== dead的行对应的动作名称（可从PlusCal生成的TLA+代码中找到该动作的定义）。如果该动作永远无法触发，TLC会报错并生成反例，反例会展示所有状态下v1始终不等于2的路径。

3. 排查初始条件与状态更新逻辑 #

• 检查初始状态是否允许v1=2：如果PlusCal代码的variables或init块中，v1的初始取值范围不包含2，该转移自然永远无法触发。
• 核对其他转移对v1的修改逻辑：如果所有其他动作都不会将v1更新为2，说明状态机逻辑里根本无法到达v1=2的状态，对应的转移必然是死代码。

4. 通过状态探索功能确认可达状态 #

在TLC的Model标签页开启「Generate States」，运行后查看所有可达状态，确认是否存在v1=2的状态。若不存在，直接说明该转移的触发条件永远无法满足。

内容的提问来源于stack exchange，提问作者milotron