TLA+入门问题：设置p3'∈0..100时不变量遭违反

核心原因 #

你遇到的问题本质是对TLA+模型检查器的检查目标和动作逻辑的误解：

• 当你将NotSolved设为不变量检查时，模型检查器会验证所有可达状态是否都满足NotSolved。但你的Next动作允许p1、p2直接跳转到0..100范围内的任意值，包括p1>p2+10且p2=10的组合（比如p1=21，p2=10），这时候NotSolved为假，模型检查器自然会报告不变量被违反。
• 你设置p3'=0时觉得“正常运行”，大概率是模型检查器的步数限制较小，没探索到违反NotSolved的状态；或者你误将“未检测到违反”当成了“程序正确”——实际上只要p1和p2能跳到满足目标条件的值，NotSolved依然会被违反。
• 仅用两个变量时无问题，可能是你当时的测试场景没触发违反路径，或是对检查结果的判断有误。

正确做法 #

根据你的需求（查找符合指定逻辑的数值），你应该检查目标状态的可达性，而非将NotSolved作为不变量：

1. 先定义目标状态：

   Solved == /\ p1 > p2 + 10 
             /\ p2 = 10
   

2. 在TLA+模型检查器中，设置检查该状态是否可达（不同工具操作略有差异，一般在“可达性检查”或“活性属性”选项中配置）。模型检查器会帮你确认是否存在路径进入Solved状态，甚至能给出具体的状态转移路径。

如果你确实需要保持NotSolved作为不变量（即确保永远不会进入目标状态），则需要修改Next动作，限制变量的变化方式，避免直接跳转到满足Solved的组合。例如，改为变量逐步增减的逻辑：

x1 == /\ p1' ∈ {p1-1, p1, p1+1} ∩ 0..100 
       /\ p2' ∈ {p2-1, p2, p2+1} ∩ 0..100
       /\ p3' ∈ {p3-1, p3, p3+1} ∩ 0..100

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