Fix a few typos and formatting errors (hwayne#36)

docs/core/concurrency.rst

@@ -251,7 +251,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 its 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 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/functions.rst

@@ -257,7 +257,7 @@ Some more examples of function sets:
 #. We have a set of servers, which can have one of three states. Then ``status \in [Server -> {"online", "booting", "offline"}]``.
 #. We represent a directed graph as a function on pairs of points, which is true iff there's an edge between the two points. Then ``graph \in [Node \X Node -> BOOLEAN]``.
 #. If we define the previous set as the operator ``GraphType``, we could get the set of all *undirected* graphs with ``{g \in GraphType: \A n1, n2 \in Node: g[n1,n2] = g[n2,n1]}``.
-#. If we have a set of users and resources, the set of all possible allocations could be ``[Resource -> User]``. If some resources could be unallocated, it would instead be ``[Resource -> User \union {NULL}]`` (where NULL is a `model value <model_value>`.
+#. If we have a set of users and resources, the set of all possible allocations could be ``[Resource -> User]``. If some resources could be unallocated, it would instead be ``[Resource -> User \union {NULL}]`` (where NULL is a `model value <model_value>`).
 
 
 .. troubleshooting::

docs/core/invariants.rst

@@ -64,7 +64,7 @@ This shows a series of steps, starting from the initial state. The top box shows
 (There's a little more we can do with the error trace, see :doc:`here </topics/toolbox>`.)
 
 
-So back to the nature of the invariant. We say ``is_unique`` is the boolean type by writing that it's an element of the set of all booleans. "Types" in TLA+s are just arbitrary sets of values. We could say that ``i`` is an integer, but we can be even more exact than that. We know that the it represents an index of ``seq``, or one past the sequence length. Its "type" is the set ``1..Len(seq)+1``. Similarly, we know ``seen`` can't have any values not in ``S``. Expanding our type invariant:
+So back to the nature of the invariant. We say ``is_unique`` is the boolean type by writing that it's an element of the set of all booleans. "Types" in TLA+ are just arbitrary sets of values. We could say that ``i`` is an integer, but we can be even more exact than that. We know that the it represents an index of ``seq``, or one past the sequence length. Its "type" is the set ``1..Len(seq)+1``. Similarly, we know ``seen`` can't have any values not in ``S``. Expanding our type invariant:
 
 ::
 
@@ -370,7 +370,7 @@ This is a common idiom for modeling simple CS algorithms. We can use the same pa
 Summary
 ========
 
-* An Invariant is something that much be true of every state in our specification.
+* An Invariant is something that must be true of every state in our specification.
 
   * A common invariant is the *Type Invariant*, which checks that all of your variable values belong to strict sets.
 

docs/core/nondeterminism.rst

@@ -146,7 +146,7 @@ If we need to also model the type of error (if that affects our recovery logic),
 
 ``either or skip`` is a common nondeterminism pattern and it's quite useful in a lot of places.
 
-We can also use nondeterminism to represent outside actions. If we're modeling requests are coming into a system, we don't need to pick a specific request to spec. Instead we can define a ``RequestType`` and pull from that on every inbound request.
+We can also use nondeterminism to represent outside actions. If we're modeling requests that are coming into a system, we don't need to pick a specific request to spec. Instead we can define a ``RequestType`` and pull from that on every inbound request.
 
 ::
 

docs/core/temporal-logic.rst

@@ -7,7 +7,7 @@ Temporal Properties
 Intro
 =======
 
-Invariants aren't really part of TLA+. There's no concept of an "invariant" that's treated as special by TLA+. The model checker, TLC, gives us that, but more that's due to pramgatics and efficiency than "invariants" being something deeply important. Rather, TLA+ provides a *general principled* way to write all kinds of different properties, where invariants are just one of many things we can check. To write these, we a set of :dfn:`temporal operators` to describe logical statements across time. We call the broad class of all properties :dfn:`temporal properties`.
+Invariants aren't really part of TLA+. There's no concept of an "invariant" that's treated as special by TLA+. The model checker, TLC, gives us that, but more that's due to pramgatics and efficiency than "invariants" being something deeply important. Rather, TLA+ provides a *general principled* way to write all kinds of different properties, where invariants are just one of many things we can check. To write these, we use a set of :dfn:`temporal operators` to describe logical statements across time. We call the broad class of all properties :dfn:`temporal properties`.
 
 .. index::
   single: safety

docs/core/tla.rst

@@ -4,7 +4,7 @@
 TLA+
 ########
 
-PlusCal is a formalism designed to make using formal methods easier. By learning pluscal first, we can focus on teaching first logic and model checking, leaving temporal logic for later. Another advantage is that can bootstrap TLA+ from it by looking at what the pluscal generates, and infer the tla+. We know that the pluscal generated is valid TLA+, so we can use it to understand the TLA+.
+PlusCal is a formalism designed to make using formal methods easier. By learning pluscal first, we can focus on teaching first logic and model checking, leaving temporal logic for later. Another advantage is that can bootstrap TLA+ from it by looking at what the pluscal generates, and infer the TLA+. We know that the pluscal generated is valid TLA+, so we can use it to understand the TLA+.
 
 .. index:: action
 
@@ -307,7 +307,7 @@ The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of
 
     Trans(state, from, to) ==
       /\ pc[state] = from
-      /\ pc' = [pc EXCEPT ![state] = 2]
+      /\ pc' = [pc EXCEPT ![state] = to]
 
     IncCounter(self) ==
       /\ Trans(self, "IncCounter", "Done")

docs/topics/aux-vars.rst

@@ -46,7 +46,7 @@ You can also use history variables to track past information no longer present i
 Error Variables
 ----------------
 
-Let's say you're writing a pluscal spec with an ``either`` branch::
+Let's say you're writing a PlusCal spec with an ``either`` branch::
 
   either
     \* path 1
@@ -55,7 +55,7 @@ Let's say you're writing a pluscal spec with an ``either`` branch::
   or
     \* ...
 
-It can be hard to tell in the error trace which branch was taken, you have to infer it from the state change. To get around this, people sometimes add lots of labels::
+It can be hard to tell in the error trace which branch was taken; you have to infer it from the state change. To get around this, people sometimes add lots of labels::
 
   either
     Path1:

docs/topics/cli.rst

@@ -50,13 +50,13 @@ TLC has other flags, but if you can't write a config format that's all moot, so
 Config Format
 .............
 
-The model checkeing config language ia special DSL for using TLC from the command line. It's what the toolbox abstracts away on the backend.
+The model checking config language is a special DSL for using TLC from the command line. It's what the toolbox abstracts away on the backend.
 
 All config files need a ``SPECIFICATION {spec}`` line, where ``Spec`` is whatever action encompasses your initial and next states. By convention, this should be called ``Spec``, but this isn't required— useful if you want different configs to test different variations of your system.
 
 Invariants you want to check must be prefixed with ``INVARIANT``, temporal properties with ``PROPERTY``. Both can have commas, eg ``INVARIANT TypeInvariant, IsSafe`` is a valid line. Unlike in the toolbox, you **cannot** make expressions invariants— they must be named operators.
 
-.. note:: Why does that work in the toolbox? When you make an expression an invariant, the Toolbox makes a separate ``MC.tla`` file, adds that expression as an operator, and then model checks ``MC.tla`` with the new operator as an invariant. It does a similar thing to get around restrictins on constant expressions, below.
+.. note:: Why does that work in the toolbox? When you make an expression an invariant, the Toolbox makes a separate ``MC.tla`` file, adds that expression as an operator, and then model checks ``MC.tla`` with the new operator as an invariant. It does a similar thing to get around restrictions on constant expressions, below.
 
 Constants are written as ``CONSTANT name = value``. Values can be simple values or sets of simple values, but not functions or expressions. To set a model value instead of an ordinary assignment, write ``CONSTANT name = name`` instead. To make a set of model values, write ``name = {a, b, c}``, where ``a, b, c`` are identifiers (**not** strings). 
 

docs/topics/tips.rst

@@ -95,6 +95,7 @@ Use the extra space in a module
 All modules have to take the form
 
 ::
+
   \* top area
   ---- MODULE name ----
   \* actual module

docs/topics/toolbox.rst

@@ -35,7 +35,7 @@ Here's a quick markup:
 3. Expands and closes all the trace steps. Good for getting a quick overview of the action flow.
 4. When toggled, clicking on an action line will automatically jump to that action in the spec. 
 
-There are also things can do by clicking on the states and values:
+There are also things you can do by clicking on the states and values:
 
 - Alt-clicking a variable hides it from the trace. To re-show it, click the filter button again. 
 - Double-clicking an action jumps to the corresponding spec code. Ctrl-doubleclicking jumps to any corresponding pluscal label.
@@ -99,15 +99,15 @@ State Constraint
 
   Liveness invariants can't be checked when the state constraint is active.
 
-  .. tip:: Use state constraints are a good way to bound unbound models.
+  .. tip:: State constraints are a good way to bound unbound models.
 
 Action Constraint
 
   Similar to a state constraint, except it's an action. In the above spec, you can write ``x' > x`` to only explore states where x increases.
 
 Definition Override
 
-  Here you can replace the definitions of some operators with custom ones. For example, if you add the definition override ``Int <- 1..10``. This is mostly often used by people who want say that a variable starts as "any integer" but limit it to a finite set for model checking.
+  Here you can replace the definitions of some operators with custom ones. For example, you can add the definition override ``Int <- 1..10``. This is mostly often used by people who want say that a variable starts as "any integer" but limit it to a finite set for model checking.
 
 
 Additional TLC Options