TLC验证通过Prop但状态END未被赋值，求技术解释

核心原因：你的Spec存在逻辑矛盾，导致其不可满足，进而使Spec => Prop成为空洞真 #

你遇到的现象是TLA+时态逻辑中的「空洞真」特性导致的——当不存在任何符合Spec的行为路径时，任何属性都会被视为“满足”，因为逻辑上「假命题蕴含任何命题」恒成立。

具体矛盾点出在你的Spec组合上：

1. [][Next]_<<s,q>>的约束：这个公式要求系统的每一步只能是Next动作，或者是不改变任何变量的「停滞步（stuttering step）」。而你的sub_nxt动作并不属于Next的一部分，也不是停滞步（它会修改变量q），因此sub_nxt是被禁止执行的。
2. SF_<<s,q>>(sub_nxt)的约束：强公平性条件要求，如果sub_nxt动作无限次处于可用状态（进入s="S1"后，sub_nxt永远可用），那么它必须被无限次执行。

这两个约束完全矛盾：前者禁止执行sub_nxt，后者要求必须无限次执行它。因此不存在任何能同时满足Spec的行为路径，Spec本身是不可满足的。此时TLC检查Spec => Prop时，会直接判定该蕴含式成立，所以报告Prop通过。

修复方案 #

根据你的需求，有两种修正方向：

1. 允许sub_nxt作为合法动作执行

将sub_nxt加入Next动作的析取中，让它成为系统允许的步骤：

Next == \/ /\ s = "S0"
           /\ s' = "S1"
           /\ UNCHANGED<<q>>
         \/ sub_nxt

此时Spec的约束不再矛盾，TLC会正确检查路径：进入s="S1"后会不断执行sub_nxt，但s永远为"S1"，因此[]<>(s = "END")会被TLC找出反例。

2. 移除不必要的公平性约束

如果你不需要强制sub_nxt被执行，直接删除Spec中的SF_<<s,q>>(sub_nxt)：

Spec == /\ Init
        /\ [][Next]_<<s,q>>

此时系统路径是：执行一次Next进入s="S1"，之后只能执行停滞步，s永远不变，TLC会生成反例证明[]<>(s = "END")不成立。

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