Declared variables found undefined during evaluation

Hi,

Attached is my TLA module, translated from PlusCal. When I run the model checker, I got the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
:
TLC cannot handle the temporal formula line 41, col 12 to line 41, col 43 of module Dum:

In evaluation, the identifier P is either undefined or not an operator.
line 41, col 24 to line 41, col 24 of module Dum

I don’t quite understand why I’m getting this error as P is declared. When I replace the P in Spec at line 41 with 1..8, the model checker runs fine.

Many thanks.

Sincerely,

Zixian

-------------------------------- MODULE Dum --------------------------------
EXTENDS Integers, Sequences, TLC, FiniteSets
(* --algorithm dum
variables N = 8,
P = 1..N;

fair process p \in P
variable n = 0
begin
A:
n := n + 1
end process

end algorithm *)
\* BEGIN TRANSLATION
VARIABLES N, P, pc, n

vars == << N, P, pc, n >>

ProcSet == (P)

Init == (* Global variables *)
/\ N = 8
/\ P = 1..N
(* Process p *)
/\ n = [self \in P |-> 0]
/\ pc = [self \in ProcSet |-> "A"]

A(self) == /\ pc[self] = "A"
/\ n' = [n EXCEPT ![self] = n[self] + 1]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << N, P >>

p(self) == A(self)

Next == (\E self \in P: p(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
/\ \A self \in P : WF_vars(p(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION
=============================================================================