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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Sun, 30 Jun 2019 01:42:11 -0500*References*: <ded66eba-ffa2-4ba0-9146-06d1e4f00210@googlegroups.com>

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.

On Sun, Jun 30, 2019, 12:31 AM Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

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 defined 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 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/CAJ-b8syp5mDQnBcrgm9yx%3DWRiWFxxzH2zMuyt6PgUXAS8xWVcQ%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] Which symbols need to be defined? (new to TLA+)***From:*Saswata Paul

**References**:**[tlaplus] Which symbols need to be defined? (new to TLA+)***From:*Saswata Paul

- Prev by Date:
**[tlaplus] Which symbols need to be defined? (new to TLA+)** - Next by Date:
**Re: [tlaplus] Which symbols need to be defined? (new to TLA+)** - Previous by thread:
**[tlaplus] Which symbols need to be defined? (new to TLA+)** - Next by thread:
**Re: [tlaplus] Which symbols need to be defined? (new to TLA+)** - Index(es):