TLA+ spec stalls as CHOOSE does not select a previous selected value

As I am starting to get used to TLA+, I started by modelling the Knight Quest problem, in which a knight must eventually reach every possible square of the chess board. For that, I've used 2 different variables: the current position and occupied set of positions.

First, I started to define my Init and Next action predicates, along with my specification and fair specification (in the WF I've only used current, as occupied may in some cases stall due to the returning to a certain position; however, if I set the WF to both, the issue is the same).

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)

Then I've set a invariant NotSolved, so TLC returns me the contraction of the invariant: in which, the occupied reaches the cardinality of (= (N-1)^2), meaning that every position was once occupied. NotSolved == Cardinality(occupied) < (N-1)^2

However, as soon as it reaches a current position, where the CHOOSE has to select a position that once was chosen (return to the same position, to then select another), the spec stalls. Which means, that the cardinality of occupied is never the same as the chess board.

I am guessing CHOOSE is the actual problem, but I am not sure how to fix this.

You are right, CHOOSE does something else than you expect. It is a function that returns an arbitrary value fulfilling the specified criteria. But because it's a function it always returns the same value for the same expression. After all you want

(CHOOSE s \in S : P(s)) = (CHOOSE s \in S : P(s))

to hold. Alternatives are usually expressed with logical disjunction ( for example Action(0) \/ Action(1) ) or the existential quantifier (for example \E s \in S: P(s) /\ Action(s) ). In your case you need to change Next to:

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

When you check for NotSolved as an invariant you will get a trace that really exceeds your size limits.

Nevertheless, the current description does allow for a path where the same element of S is chosen over and over again. You can prevent that by adding /\ ~(Chosen \in occupied) as a conjunct. But that also means at some point you will have exhausted S and your algorithm will stall which you need to take into account.