[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Which symbols need to be defined? (new to TLA+)

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  

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ded66eba-ffa2-4ba0-9146-06d1e4f00210%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.