A set of suggestions and confusing bits

[kkredit]

This is a set of all the suggestions I had or confusing things I noticed during a read-through. I hope you don't mind the list of unrelated items here, but I didn't want to spam the issues board. I know this is very much a work in progress so some issues aren't unexpected -- thanks for making this resource, and take or leave these suggestions as you wish.

1. I thought it would be worth mentioning that pc probably stands for program counter.
2. A sentence in "Writing an Invariant > Quantifiers" says "That's for two reasons", but then the text appears to give three reasons.
3. The fact that A => B is equivalent to ~A \/ B was the most helpful piece to help me understand =>. Many programmers are already have an intuition for this form. It could be just me, but explaining it like "~A \/ B is really helpful, so TLA+ gives us syntactic sugar in the form of =>" would make for a more natural explanation. Just something to consider.
4. "State sweeping" is defined twice in the Tip in the Structured Data chapter ("State sweeping is when...", then "... trick known as state sweeping").
5. In "Temporal Properties > Strong Fairness", <> is used in an example spec before it is defined.
6. In "TLA+ > Fairness in TLA+", the fairness definitions use WF_v and SF_v, but the English explanation uses WF_x and WF_vars. This is kind of confusing. Does it matter?
7. Related to the previous comment, a discussion of how TLA+ treats underscores might be helpful. It is very surprising that underscores convey meaning. In every language I've used, they are just identifier characters, but in TLA+ they seem to be used as some sort of special separator. Is that right? Some clarification might be helpful.
8. <=> is used in "General Tips" and /= in the Goroutines example without either being defined. (The /= looks like it could be #?)
9. In "Using the Toolbox > Module Configuration" there is an unfinished sentence: "On the Model Overview page of a model, there are three This is not comprehensive."

[hwayne]

Thanks for these suggestions! I plan to look at them all this week.

[hwayne]

Ugh finally looking at it late

---

• [x] I thought it would be worth mentioning that pc probably stands for program counter.
• [x] <=> is used in "General Tips" and /= in the Goroutines example without either being defined. (The /= looks like it could be #?)
• [x] A sentence in "Writing an Invariant > Quantifiers" says "That's for two reasons", but then the text appears to give three reasons.
• [x] "State sweeping" is defined twice in the Tip in the Structured Data chapter ("State sweeping is when...", then "... trick known as state sweeping").
• [x] In "Temporal Properties > Strong Fairness", <> is used in an example spec before it is defined.
• [x] In "Using the Toolbox > Module Configuration" there is an unfinished sentence: "On the Model Overview page of a model, there are three This is not comprehensive."
• [x] In "TLA+ > Fairness in TLA+", the fairness definitions use WF_v and SF_v, but the English explanation uses WF_x and WF_vars. This is kind of confusing. Does it matter?
• [ ] The fact that A => B is equivalent to ~A \/ B was the most helpful piece to help me understand =>. Many programmers are already have an intuition for this form. It could be just me, but explaining it like "~A \/ B is really helpful, so TLA+ gives us syntactic sugar in the form of =>" would make for a more natural explanation. Just something to consider.
• [ ] Related to the previous comment, a discussion of how TLA+ treats underscores might be helpful. It is very surprising that underscores convey meaning. In every language I've used, they are just identifier characters, but in TLA+ they seem to be used as some sort of special separator. Is that right? Some clarification might be helpful.

[federicobond]

This one can be ticked off now:

In "TLA+ > Fairness in TLA+", the fairness definitions use WF_v and SF_v, but the English explanation uses WF_x and WF_vars. This is kind of confusing. Does it matter?