TLA+骑士巡游建模停滞：CHOOSE未选已选值问题求助

背景 #

刚接触TLA+，尝试建模骑士巡游问题（要求骑士最终遍历棋盘所有方格），用了两个变量：current表示当前位置，occupied记录已访问的位置集合。

现有建模代码 #

CONSTANT N
VARIABLE occupied, current
vars    == << occupied, current >>
Possible == 0..N-1

Inv    == /\ Cardinality(occupied) \leq N^2
          /\ IsFiniteSet(occupied)
          /\ occupied \subseteq (Possible \X Possible)

Jumps(pair) == LET x == pair[1]
                   y == pair[2] 
                IN 
                ({<<x+2, y-1>>, <<x+2, y+1>>, <<x-2,y+1>>, <<x-2,y-1>>}
                    \cup
                 {<<x+1, y-2>>, <<x+1, y+2>>, <<x-1,y+2>>, <<x-1,y-2>>}
                ) 
                    \cap 
                (Possible \X Possible)

Init == \E x \in Possible     : \E y \in Possible : /\ occupied = {<<x,y>>}
                                                    /\ current  = <<x,y>>

Next == LET S == Jumps(current) 
            Chosen == CHOOSE s \in S: TRUE
        IN
            /\ current'  = Chosen
            /\ occupied' = occupied \cup {Chosen}

Spec      == Init /\ [][Next]_vars
FairSpec  == Spec /\ WF_occupied(Next)

遇到的问题 #

设置了不变量NotSolved，想让TLC返回反例（即遍历完成的路径）：

NotSolved == Cardinality(occupied) < (N-1)^2

但运行时发现，当current处于某个位置时，CHOOSE会选中已访问过的位置，之后规范就停滞了，occupied的基数永远到不了棋盘总方格数。猜测问题出在CHOOSE算子上，但不知道怎么修复。

问题根源与修复方案 #

问题根源 #

CHOOSE s ∈ S: TRUE是确定性选择——只要集合S非空，TLA+会固定选中S里的某一个元素。如果这个元素已经在occupied中，后续的Next动作只会重复跳到同一个位置，occupied不再增长，直接导致规范停滞。

修复步骤 #

1. 修改Next动作，实现非确定性选择
   要让骑士每次能选择所有未访问的合法跳跃位置，用存在量词\E来枚举所有可能的选择，而不是固定选一个：

   Next == LET S == Jumps(current)
               Unvisited == S \ occupied
               // 优先选未访问的位置；遍历完成后可任意跳，不影响结果
               ChosenSet == IF Unvisited # {} THEN Unvisited ELSE S
           IN
               \E s ∈ ChosenSet:
                   /\ current' = s
                   /\ occupied' = occupied ∪ {s}
   

2. 调整公平性规范
   原来的WF_occupied(Next)不合适，因为occupied只有在选中新位置时才会变化。应该用WF_vars(Next)，确保只要有合法跳跃动作可执行，就一定会执行：

   FairSpec == Spec /\ WF_vars(Next)
   

3. 修正不变量的目标
   你写的NotSolved目标错误，棋盘总方格数是N^2，应该改成：

   NotSolved == Cardinality(occupied) < N^2
   

   这样当骑士遍历完所有位置时，这个不变量会被违反，TLC会返回完整的巡游路径作为反例。

额外说明 #

• TLA+的CHOOSE算子适合需要固定选择某个元素的场景，建模非确定性动作（比如骑士的可选移动）必须用\E来表示所有可能的选项。
• 当所有位置都被访问后，Next动作仍可执行（重复跳跃），但此时occupied不再变化，不会影响我们验证“是否存在完整巡游路径”的目标。

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