In page 11 of the TLA+ hyperbook, it is clearly stated that "Every symbol that appears in the module must either be a primitive TLA+ operator or else de fined or declared before its first use.". However, in the example given in the site
https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html, the symbols p and q have not been declared or defined before use. So can someone clarify how we can understand which symbols need to be declared and which do not?
PS: The example code from the site:
-------------------- MODULE Euclid --------------------
EXTENDS Integers
p | q == \E d \in 1..q : q = p * d
Divisors(q) == {d \in 1..q : d | q}
Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y
GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))
Number == Nat \ {0}
CONSTANTS M, N
VARIABLES x, y
Init == (x = M) /\ (y = N)
Next == \/ /\ x < y
/\ y' = y - x
/\ x' = x
\/ /\ y < x
/\ x' = x-y
/\ y' = y
Spec == Init /\ [][Next]_<<x,y>>
ResultCorrect == (x = y) => x = GCD(M, N)
THEOREM Correctness == Spec => []ResultCorrect
=======================================================