Fixed typos and language in documentation

docs/core/concurrency.rst

@@ -35,7 +35,7 @@ Now let's add another process that reads from the queue.
 
   Different processes cannot share label names.
 
-The writer has a single action, ``Write``, and the reader has a single action, ``Read``. We haven't specified which should happen first, so the two can happen in any order. Either we (1) write to the queue and then read from it, or (2) read from the queue and then write to it.
+The writer has a single action, ``AddToQueue``, and the reader has a single action, ``ReadFromQueue``. We haven't specified which should happen first, so the two can happen in any order. Either we (1) write to the queue and then read from it, or (2) read from the queue and then write to it.
 
 Behavior (2) doesn't make any sense: how can we read from the queue if there's nothing already in it? And if you try to run the spec, TLC will raise this as an error.
 
@@ -118,7 +118,7 @@ Notice how many more states we have. The ``while`` loop is nonatomic, and every
   :diff: reader_writer/rw_local_1/reader_writer.tla
   :ss: rw_local_2
 
-As with global variables, we can have multiple starting local variables— ``i \in 1..3`` is valid.
+As with global variables, we can have multiple starting local variables — ``i \in 1..3`` is valid.
 
 In practice, local variables aren't often used, as operators in `define <define>` blocks can't use them. This means you can't easily typecheck them, write helper operators, etc. Generally we use local variables as :ref:`auxiliary <topic_aux_vars>` or "bookkeeping" variables, like loop iterations and model bounding.
 
@@ -155,7 +155,7 @@ This is equivalent to putting the label in a ``while TRUE`` loop.
 
 .. rubric:: ``self``
 
-In process sets we have a special keyword ``self``, which retrieves the "value" of the process. So for the writers, the values of the process would be ``1`` and ``2``. If we tell the writers to put ``self`` on instead of ``1``, we'd expect the end total to be 6.
+In process sets we have a special keyword ``self``, which retrieves the "value" of the process. So for the writers, the values of the process would be ``1``, ``2`` and ``3``. If we tell the writers to put ``self`` on instead of ``1``, we'd expect the end total to be 6.
 
 .. spec:: reader_writer/rw_many_3/reader_writer.tla
   :diff: reader_writer/rw_many_2/reader_writer.tla
@@ -197,11 +197,11 @@ In real systems you often have *bounded* queues, which prevent writes when they'
   :diff: reader_writer/rw_many_3/reader_writer.tla
   :ss: rw_await
 
-``await`` is a *restriction* on when the label can run. The label can only run— the state "committed", if you will— if *every* ``await`` statement in the label evaluates to true.
+``await`` is a *restriction* on when the label can run. The label can only run — the state "committed", if you will — if *every* ``await`` statement in the label evaluates to true.
 
 .. note:: `with <nondet_with>` ``x \in set`` also blocks if the set is empty.
 
-.. warning:: ``await`` interacts a little oddly with variable updates— it will be based on the updated value if directly embedded but not if the variable is used via a ``defined`` operator. This is due to the PlusCal->TLA+ translation grammar. As a general precaution, don't use updated variables in ``await`` statements.
+.. warning:: ``await`` interacts a little oddly with variable updates — it will be based on the updated value if directly embedded but not if the variable is used via a ``defined`` operator. This is due to the PlusCal->TLA+ translation grammar. As a general precaution, don't use updated variables in ``await`` statements.
 
 .. index:: Deadlocks
 .. _deadlock:
@@ -249,7 +249,7 @@ The thread-local variable is an "internal implementation detail", and I don't th
 
 Before we continue, I want to recommend a good exercise to improve your modeling skills. You know, based on how I'm presenting this example, that this will fail. But *how* will it fail? Before you run the model checker, try to figure out what error it will give you and why. See if you can guess the number of steps it will take, and what order the processes will run.
 
-This is will help you get better with TLA+, but it does something else, too. As you write more specifications, you'll start to see errors *without* running the model checker. One reason why concurrency is so unintuitive is we normally don't get rapid feedback on the mistakes we make. If you had a race condition to your code, it could be days or weeks before bites you, and then it takes even longer to fully understand it. Whereas in a specification, the model checker shows you immediately. This trains your intuition for race conditions much more quickly than normal.
+This is will help you get better with TLA+, but it does something else, too. As you write more specifications, you'll start to see errors *without* running the model checker. One reason why concurrency is so unintuitive is we normally don't get rapid feedback on the mistakes we make. If you had a race condition to your code, it could be days or weeks before it bites you, and then it takes even longer to fully understand it. Whereas in a specification, the model checker shows you immediately. This trains your intuition for race conditions much more quickly than normal.
 
 ...
 

docs/core/constants.rst

@@ -67,7 +67,7 @@ If you have a spec with constants, you should put constraining assumptions on th
 Model Values
 ----------------
 
-That takes care of ordinary assignments, what about "model values"? Model values are a special type of value in TLA+. A model value has no operations and can only be tested for equality, and is only equal to itself. IE
+That takes care of ordinary assignments, what about "model values"? Model values are a special type of value in TLA+. A model value has no operations and can only be tested for equality, and is only equal to itself.
 
 .. code-block::
 
@@ -113,7 +113,7 @@ We can also assign constants to sets of model values. Put it in as a normal set,
   S <- [model value] {s1, s2, s3, s4, s5}
 
 
-Sets of model values will become *extremely* useful when we start modeling :doc:`concurrency <concurrency>`, but there's still one cool trick we can do with them right now. If you run the model with that value of ``S``, you will get 4,375 states total— the same as if you did ``S <- 1..5``. But notice this other option below the "set of model values" bar:
+Sets of model values will become *extremely* useful when we start modeling :doc:`concurrency <concurrency>`, but there's still one cool trick we can do with them right now. If you run the model with that value of ``S``, you will get 4,375 states total — the same as if you did ``S <- 1..5``. But notice this other option below the "set of model values" bar:
 
 .. image:: img/symmetry_set.png
 

docs/core/functions.rst

@@ -102,7 +102,7 @@ The set we're mapping from, ``S``, is the **domain** of the function, and can be
 1. A sequence is just a function where the domain is ``1..n``.
 2. A struct is just a function where the domain is a set of strings.
 
-But functions are a more general than that, and can map *any* set of values. For example, we can have pairs of numbers in the domain of the function.
+But functions are more general than that, and can map *any* set of values. For example, we can have pairs of numbers in the domain of the function.
 
 ::
 
@@ -194,7 +194,7 @@ We can check that these are equivalent by writing a quantifier check:
 Using Functions
 -----------------
 
-Why functions over operators? We rarely use functions for computations— operators are far superior for that. Functions are important as *values*. We can assign them to variables and manipulate them like any other value.
+Why functions over operators? We rarely use functions for computations - operators are far superior for that. Functions are important as *values*. We can assign them to variables and manipulate them like any other value.
 
 In a spec I once wrote, I had to assign tasks to CPUs. Some tasks needed to be assigned to many CPUs, but each CPU should only have one task. In that spec, the best solution was to store assignments as functions, where each task mapped to a set of CPUs.
 
@@ -271,11 +271,11 @@ Some more examples of function sets:
 
     Encountered "\|->" in line X, column Y
 
-  In a function set, then you probably wrote ``[S |-> T]`` instead of ``[S -> T]``. Similarly, if you get
+  in a function set, then you probably wrote ``[S |-> T]`` instead of ``[S -> T]``. Similarly, if you get
 
     Encountered "->" in line X, column Y
 
-  In a function, then you probably wrote ``[x \in S -> T]`` instead of ``[x \in S |-> T]``. Don't worry, everybody gets the two mixed up at some point.
+  in a function, then you probably wrote ``[x \in S -> T]`` instead of ``[x \in S |-> T]``. Don't worry, everybody gets the two mixed up at some point.
 
 .. rubric:: Example: Sorting
 
@@ -320,7 +320,7 @@ To figure out if two sequences have the same number of each element, let's defin
   CountMatching(f, val) ==
     Cardinality({key \in DOMAIN f: f[key] = val})
 
-Then we just need to test to check this over every element in the sequence:
+Then we just need to check this over every element in the sequence:
 
 ::
 

docs/core/invariants.rst

@@ -44,7 +44,7 @@ This operator needs to know about the ``is_unique`` variable, so we have to put
   :diff: duplicates/3/duplicates.tla
   :ss: duplicates_many_inputs
 
-To check this, we add it as an :doc:`invariant <setup>`. TLC will check it at every possible state. All of the invariants passing looks the same as us not having any invariants— TLC will only do something interesting if the invariant fails. Here's what happens if we instead change the invariant to ``is_unique = TRUE``:
+To check this, we add it as an :doc:`invariant <setup>`. TLC will check it at every possible state. All of the invariants passing looks the same as us not having any invariants — TLC will only do something interesting if the invariant fails. Here's what happens if we instead change the invariant to ``is_unique = TRUE``:
 
 .. figure:: img/invariants_fail.png
 
@@ -95,9 +95,9 @@ We can simplify this by just using ``=``.
 Now the next two steps:
 
 1. Actually implement ``IsUnique(s)``.
-2. Currently, ``is_unique`` starts out true and flips to false if we find a duplicate. If the sequence *isn't* unique, then the invariant would fail as soon as we start— ``is_unique`` is true but ``IsUnique(seq)`` will be false. So we only want to check the "invariant" after the algorithm finishes running.
+2. Currently, ``is_unique`` starts out true and flips to false if we find a duplicate. If the sequence *isn't* unique, then the invariant would fail as soon as we start — ``is_unique`` is true but ``IsUnique(seq)`` will be false. So we only want to check the "invariant" after the algorithm finishes running.
 
-Writing ``IsUnique(s)`` *properly* requires learning some things. Writing it *improperly* is possible though, so let's start with that, then cover (2), the double back to doing ``IsUnique`` properly.
+Writing ``IsUnique(s)`` *properly* requires learning some things. Writing it *improperly* is possible though, so let's start with that, then cover (2), then double back to doing ``IsUnique`` properly.
 
 Here's the improper solution for ``IsUnique``:
 

docs/core/nondeterminism.rst

@@ -173,7 +173,7 @@ One way we use nondeterminism is to simulate user input. Our system has to handl
 .. spec:: calculator/1/calculator.tla
   :name: calculator_1
 
-.. todo:: This example might work better if I break the ``while`` into a separate step. But that's for after v2 is up and I'm polishing— might be totally unnecessary.
+.. todo:: This example might work better if I break the ``while`` into a separate step. But that's for after v2 is up and I'm polishing — might be totally unnecessary.
 
 Two things to notice:
 

docs/core/operators.rst

@@ -123,7 +123,7 @@ A quick mnemonic: ``~`` is a little flippy thing, so it's "not". ``/\`` looks li
 .. index:: => (implies)
 .. _=>:
 
-There is one more boolean operator of note: ``=>``, or "implication". ``A => B`` means "A is at least as true as B". ``A => B = FALSE`` when false if A is true and B is false, otherwise it's true. B is true or A is false (or both). You don't see this very often in programming, as it's pretty useless for control flow. But it's *extremely* important for any kind of specification work. We'll go into more detail about it `later <using_=>>`. [#iff]_
+There is one more boolean operator of note: ``=>``, or "implication". ``A => B`` means "A is at least as true as B". ``A => B = FALSE`` if A is true and B is false, otherwise it's true. You don't see this very often in programming, as it's pretty useless for control flow. But it's *extremely* important for any kind of specification work. We'll go into more detail about it `later <using_=>>`. [#iff]_
 
 .. exercise:: Contrapositives
   :name: contrapositive
@@ -527,5 +527,5 @@ Summary
   - We can map and filter sets.
 
 
-.. [#except-strings] Except strings. Well actually there is a keyword, ``STRING``, but it represents all possible strings, which is an infinitely large set, so...
 .. [#iff] There's also ``A <=> B`` for "A and B are both true or both false", but it's the same thing as writing ``A = B``.
+.. [#except-strings] Except strings. Well actually there is a keyword, ``STRING``, but it represents all possible strings, which is an infinitely large set, so...

docs/core/pluscal.rst

@@ -168,7 +168,7 @@ if
   end if;
 
 
-You *can* put labels inside an if block. This is useful if your logic branches, and some of the branches represent more complicated behavior. You don't need to balance the labels in an if block— some conditionals can have labels and others do not. **However, if any branch has a label, you must follow the entire block with a label**. To see why, consider the following:
+You *can* put labels inside an if block. This is useful if your logic branches, and some of the branches represent more complicated behavior. You don't need to balance the labels in an if block — some conditionals can have labels and others do not. **However, if any branch has a label, you must follow the entire block with a label**. To see why, consider the following:
 
 ::
 
@@ -328,7 +328,7 @@ To check both, we can use multiple starting states. TLA+ doesn't just let us ass
 .. spec:: duplicates/2/duplicates.tla
   :diff: duplicates/1/duplicates.tla
 
-The model checker will now check *both* ``<<1, 2, 3, 2>>`` and ``<1, 2, 3, 4>>`` as the value of ``seq``. More specifically, does two complete runs, one for each possible value. If either complete run, or :dfn:`behavior`, would lead to an error, TLC will let us know.
+The model checker will now check *both* ``<<1, 2, 3, 2>>`` and ``<1, 2, 3, 4>>`` as the value of ``seq``. More specifically, it does two complete runs, one for each possible value. If either complete run, or :dfn:`behavior`, would lead to an error, TLC will let us know.
 
 .. figure:: graphs/duplicates_2.gv.png
 
@@ -372,7 +372,7 @@ Summary
 
 - Specifications have variables. These can either be a fixed value (using ``=``) or an element in a set (using ``\in``). Any TLC value can be a variable.
 
-  - If an element of a set, then TLC will test the model on *every possible starting state*.
+  - If a variable is an element of a set, then TLC will test the model on *every possible starting state*.
 - PlusCal is a language that makes writing specifications easier.
 
   - In the PlusCal algorithm body, variables are updated with ``:=``. ``=`` is comparison.

docs/core/temporal-logic.rst

@@ -66,7 +66,7 @@ At the beginning of the behavior, we pick one online server. That server is then
 
 .. figure:: graphs/liveness.gv.png
 
-  The behavior sequence 1-2-3 breaks violates our safety property, even though no state is individually a "bad state".
+  The behavior sequence 1-2-3 violates our safety property, even though no state is individually a "bad state".
 
 In summary, adding ``[]`` to the language lets us represent all invariants, and a host of other properties too.
 
@@ -105,7 +105,7 @@ Not so fast! There's a *third* thing the orchestrator can do: it can crash. In T
 
 .. note:: Why haven't we see this before? Because up until now we've only had invariants, which are only violated by "bad states": particular configurations of variables that break the invariants. Stutter steps don't change the values of anything, so a stutter step can never break an invariant. Here's the first time it can break things by *preventing* us from reaching a good state.
 
-TLA+ allows infinite stutter steps because it is fundamentally a worst-case scenario language. IN reality, systems always crash. If we do not *explicitly say* a system can't crash, TLA+ will assume the system can crash at the worst possible time.
+TLA+ allows infinite stutter steps because it is fundamentally a worst-case scenario language. In reality, systems always crash. If we do not *explicitly say* a system can't crash, TLA+ will assume the system can crash at the worst possible time.
 
 .. figure:: graphs/stuttering.gv.png
 

docs/core/tla.rst

@@ -298,12 +298,12 @@ Looking it at piece-by-piece:
                       /\ pc' = [pc EXCEPT ![self] = "Done"]
 
 
-The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of it, it sets ``pc[self]`` to "Done". That's how we emulate sequentiality in TLA+ algorithm— it's like going from the "IncCounter" label to the "Done" label. Each label corresponds to exactly one action, and vice versa.
+The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of it, it sets ``pc[self]`` to "Done". That's how we emulate sequentiality in TLA+ algorithm — it's like going from the "IncCounter" label to the "Done" label. Each label corresponds to exactly one action, and vice versa.
 
 .. _trans:
 .. tip::
 
-  The PlusCal to TLA+ translator is very simple. If we were writing the TLA+ from scatch, we could use a helper action to these transitions look cleaner:
+  The PlusCal to TLA+ translator is very simple. If we were writing the TLA+ from scatch, we could use a helper action to make these transitions look cleaner:
 
   ::
 

docs/index.rst

@@ -20,7 +20,7 @@
 Learn TLA+
 ====================================
 
-Most software flaws come from one of two places. A code bug is when the code doesn't match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we're just taught to "think about it really hard".
+Most software flaws come from one of two places. A code bug is when the code doesn't match our design — for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we're just taught to "think about it really hard".
 
 TLA+ is a "formal specification language", a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and CrowdStrike. TLA+ doesn't replace our engineering skill but *augments* it. With TLA+ we can design systems faster and more confidently. Check out the `chapter_overview` to see an example of this in practice.
 

docs/topics/aux-vars.rst

@@ -66,7 +66,7 @@ It can be hard to tell in the error trace which branch was taken; you have to in
   or
     \* ...
 
-Then you can see which path you took in ``pc``. But doing this adds a lot of extra concurrency to your spec— at best exploding the state space, at worst changing the spec semantics!
+Then you can see which path you took in ``pc``. But doing this adds a lot of extra concurrency to your spec — at best exploding the state space, at worst changing the spec semantics!
 
 What we want is to enrich the error traces without changing the spec semantics. This is a great place for an aux var.