| Think of the line
p | q == \E d \in 1..q : q = p * d
as defining an operator
div(p,q) == ...
with two parameters p and q. TLA+ has support for (certain) symbols being used as infix operators.
Stephan
In the example, p and q are symbols which have been used to define the infix operator |. However, they have not been declared or defined before use. Whereas, M, N, x, and y have been defined/declared before using them. My question is, why do M, N, x, and y require a declaration while p and q don't? Aren't they all symbols? Are you talking about this line?
p | q == \E d \in 1..q : q = p * d
That's defining the infix operator |, so p and q are the parameters.
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.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/jXBjiUjfXqY/unsubscribe.
To unsubscribe from this group and all its topics, 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/CAJ-b8syp5mDQnBcrgm9yx%3DWRiWFxxzH2zMuyt6PgUXAS8xWVcQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
--
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/CAHeFUE_ygwU5LBdOARdiATxrDVJVv0WPW7ug5FW3twcrPA9w1w%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
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/ED7EAA86-9410-47A1-BBBB-F2EAAE71AE69%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
|