general improvements

docs/_static/custom.css

@@ -1,9 +1,5 @@
 @import 'basic_mod.css';
 
-.code-block-caption {
-  text-align: center;
-}
-
 blockquote.quote {
   border-left: .2em solid #bdbdbd;
   font-style: italic;
@@ -23,11 +19,11 @@ div.document h2, div.document h3, div.document h4, .rubric {
 }
 
 div.document div.admonition.warning {
-  border-left: 5px solid red;
+  border-left: 5px solid crimson;
 }
 
 div.document div.admonition.warning p.admonition-title {
-  color: red;
+  color: crimson;
 }
 
 .caption-number {
@@ -36,3 +32,19 @@ div.document div.admonition.warning p.admonition-title {
  */
   display: none;
 }
+
+/* span.caption-text */
+.code-block-caption {
+  text-align: center;
+}
+
+
+figure img {
+  border: 1px;
+}
+
+figcaption p {
+  margin-top: 8px;
+  text-align: center;
+
+}

docs/beginner/invariants.rst

@@ -43,13 +43,12 @@ This operator needs to know about the ``all_unique`` variable, so we have to put
 .. spec:: duplicates/inv_1/duplicates.tla
   :diff: duplicates/3/duplicates.tla
   :ss: duplicates_many_inputs
-  :caption: blah
 
-To check this, we add it as an `invariant <chapter_setup>`. TLC will check it for every possible state :ss:`duplicates_many_inputs`. 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 ``all_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 ``all_unique = TRUE``:
 
-.. todo:: img
+.. todo:: {SCREENSHOT}
 
-.. todo:: talk about the error trace
+.. todo:: {CONTENT} talk about the error trace
 
   There's a little more we can do with the error trace, see here.
 
@@ -97,10 +96,11 @@ Here's the improper solution for ``IsUnique``:
 
 If the sequence has duplicates, then we won't run the ``\union`` line every single time, so it will have a different cardinality. In the next section, we'll see why this is "improper" and implement it properly, but for now this opens up our ability to discuss (2).
 
-.. note:: Also, because sets are unique.
+.. note:: This works because sets are unique.
+
 
 .. index:: pc
-  :name: pc
+.. _pc:
 
 pc
 ....
@@ -115,6 +115,8 @@ You can see this in the error trace. When we start the algorithm, ``pc = "Iterat
 
 On every label *except* "Done", this evaluates to TRUE and the invariant passes. When it *is* "Done", then we check the condition we care about.
 
+.. index:: => (implies)
+
 ``IF A THEN B ELSE TRUE`` conditionals come up a lot, cases where we only want to check B if A is true. Another way of saying this "either B is true or A is false".
 
 Another way of writing this: ``A => B``. Either B is true or A is false. Now we have
@@ -123,9 +125,7 @@ Another way of writing this: ``A => B``. Either B is true or A is false. Now we
 
   IsCorrect == pc = "Done" => is_unique = IsUnique(seq)
 
-I said ``=>`` was really important earlier. This is one of those ways: it lets us say invariants should only apply under certain conditions. This isn't the only place we might use it.
-
-.. todo:: hascredential => TK EXAMPLES
+I said ``=>`` was really important earlier. This is one of those ways: it lets us say invariants should only apply under certain conditions. 
 
 We can now run this as our full invariant, and the spec works :ss:`duplicates_many_inputs`. 
 
@@ -198,8 +198,8 @@ That suggests we can write ``IsUnique`` as
 
 .. _implication_2:
 
-The power of ``=>``
----------------------
+The power of :math:`\Rightarrow`
+---------------------------------
 
 Let's add this new version of ``IsUnique`` to our duplicates spec:
 
@@ -329,45 +329,46 @@ This should pass :ss:`duplicates_many_inputs`.
       \E i, j \in 1..Len(seq):
         i # j /\ seq[i] = seq[j]
 
-More invariant practice
-------------------------
+.. todo::
 
-.. todo:: Find actual names for everything
+  .. rubric:: More invariant practice
 
-Consider we have an event queue of events that happen in a system, where the queue is represented by a sequence of strings. One of teh invariants of the system is that "A can only come after B if the D flag is set."
+  .. todo:: Find actual names for everything
 
-Properties of the form "X can only be true if Y is also true" can be written as ``X => Y``. To see why, try writing out the truth table.
+  Consider we have an event queue of events that happen in a system, where the queue is represented by a sequence of strings. One of teh invariants of the system is that "A can only come after B if the D flag is set."
 
-So we have:
+  Properties of the form "X can only be true if Y is also true" can be written as ``X => Y``. To see why, try writing out the truth table.
 
-::
+  So we have:
 
-  Inv == IsAfter(A, B) => D
+  ::
 
-That just leaves specifying ``IsAfter``. 
+    Inv == IsAfter(A, B) => D
 
-::
+  That just leaves specifying ``IsAfter``. 
+
+  ::
 
-  \* Test this
+    \* Test this
 
-  IsAfter(seq, e1, e2) ==
-    \E i, j \in 1..Len(seq):
-      /\ i > j
-      /\ seq[i] = e1
-      /\ seq[j] = e2
+    IsAfter(seq, e1, e2) ==
+      \E i, j \in 1..Len(seq):
+        /\ i > j
+        /\ seq[i] = e1
+        /\ seq[j] = e2
 
 
-.. todo:: 
+  .. todo:: 
 
-  .. rubric:: More invariant practice
+    .. rubric:: More invariant practice
 
-  ``=>`` is extremely powerful, so let's spend more time working with it. How would we write an operator that tests if a sequence is sorted in ascending order? What would ``IsSorted(seq)`` look like,
+    ``=>`` is extremely powerful, so let's spend more time working with it. How would we write an operator that tests if a sequence is sorted in ascending order? What would ``IsSorted(seq)`` look like
 
-  ::
+    ::
 
-    IsSorted(seq) ==
-      \A i, j \in 1..Len(seq):
-        i < j => seq[i] <= seq[j]
+      IsSorted(seq) ==
+        \A i, j \in 1..Len(seq):
+          i < j => seq[i] <= seq[j]
 
 
 When to use Invariants

docs/beginner/operators.rst

@@ -80,6 +80,8 @@ Every value type in TLA+ has its own operators, with no overlap or overloading.
   It's likely because you used a double ``==`` instead of a single ``=`` when testing for equality.
 
 
+.. _string:
+
 The obvious ones
 ----------------
 
@@ -214,15 +216,17 @@ Some programming languages have sets, but they're often less important than arra
 .. index:: set; set operators, \in; x \in set
 .. _set_operators:
 
-Operators
-----------
+Set Operators
+--------------
 
 The main thing we do with sets is check if some values belong to it. We do this with ``\in``: ``x \in set`` is true iff ``x`` is an element of ``set``. ``\in`` is also used in a few other places as syntax, not just as an operator. There's also the inverse, ``\notin``.
 
 * ``set1 \subseteq set2`` tests if every element of ``set1`` is also an element of ``set2``.
 
     .. note:: That's "subset or equals". It's a way to sidestep the question "Is a set a subset of itself?"
 
+.. index:: \ (set difference)
+
 We also have ways of slicing and dicing sets:
 
 * ``set1 \union set2`` is the set of all elements in ``set1`` or ``set2`` (or both).
@@ -316,29 +320,19 @@ Sets can be mapped and filtered.
 
 I've found that the best way to remember which is which is by reading the colon as a "where". So the map is "x squared where x in 1..4", while the filter is "x in 1..4 where x is even".
 
-.. .. exercise:: taba
-  :label: asdasd
-
-  #. Using ``ClockType`` as the set of all valid times, use a filter to get all of the times before noon (``<<12, 0, 0>>``)
-
-  #. ???
-
-  .. ``{t \in ClockType: t[1] < 12}``
+To get all the times half-past the hour, we could write:
 
-  .. ordered pairs
+::
 
+  {t \in ClockType: t[2] = 29 /\ t[3] = 0}
 
 
-.. .. exercise:: Sequence Manipulations
-    :label: map_filter_seq
+Map and filter are great for utility, too. The *range* of a sequence is the set of all elements in the sequence. We can get that with a set map:
 
-    1. Write ``IndicesMatching(seq, val)``, which returns all indices ``i`` of ``seq`` where ``seq[i] = val``.
-    2. Write ``Range(seq)``, which returns all values in ``seq``. IE ``Range(<<"a", "b", "a">>) = {"a", "b"}``.
+::
 
-  .. solution:: map-filter-seq
+  Range(seq) == {seq[i]: i \in 1..Len(seq)}
 
-    1. ``IndicesMatching(seq, val) == {i \in 1..Len(seq): seq[i] = val}``
-    2. ``Range(seq) == {seq[i]: i \in 1..Len(seq)}``
 
 .. index:: CHOOSE, \in; x \in set
 
@@ -351,7 +345,7 @@ Getting the number of seconds past midnight from a clock value is straightforwar
 
 #. Floor divide by 60 to get the total minutes, and then set the remainder as "seconds".
 #. Floor divide again by 60 to get the total hours.
-#. Set the remainder of the second divison as minutes.
+#. Set the remainder of the second division as minutes.
 
 .. todo:: Talk about how this can give you ``<<25, 0, 0>>`` as a value
 
@@ -371,7 +365,7 @@ We don't do it this way because "the set of all possible clock values" is over 8
 CHOOSE is useful whenever we need to pull a value from a set.
 
 Now what happens if we write ``ToClock(86401)``? There are no clock times that have 86,401 seconds. If you try this, TLC will raise an error. This is in contrast to the implementation solution, which will instead give us a nonsense value. 99% of the time if it can't find a corresponding element of the set, that's a bug in the specification, an edge case you didn't consider. Better to harden up the operator:
-{{Notice this is more stricter than the constructive solution, which would isntead give you junk values}}
+{{Notice this is more stricter than the constructive solution, which would instead give you junk values}}
 
 ::
 
@@ -394,8 +388,9 @@ Now what happens if we write ``ToClock(86401)``? There are no clock times that h
 
   What if multiple values satisfy ``CHOOSE``? In this case the only requirement is that the result is *deterministic*: the engine must always return the same value, no matter what. In practice this means that TLC will always choose the lowest value that matches the set.
 
-.. index:: LET
 
+
+.. index:: LET
 .. _LET:
 
 LET
@@ -413,30 +408,51 @@ The LET gives us a new definition, locally scoped to ``ToClock``. ``seconds_per_
 
 Wait, operator? Yes, we can add parameterized operators in ``LET``, too!
 
-.. todo:: 
+::
 
-    Clamp(min, val, max) ==
-
-
+   ThreeMax(a, b, c) ==
+      LET
+        Max(x, y) == IF x > y THEN x ELSE y
+      IN
+        Max(Max(a, b), c)
+
+And you can define multiple operators in the same LET:
+
+::
+
+   ThreeMax(a, b, c) ==
+      LET
+        Max(x, y) == IF x > y THEN x ELSE y
+        maxab == Max(a, b)
+      IN
+        Max(maxab, c)
 
 Each operator in the LET can refer to previously defined operators in that scope. With this we can construct solutions step-by-step. 
 
 If you have to write a complex operator, breaking it into steps with LET is a great way to make it more understandable.
 
-.. todo:: Something on nesting expressions
-
 Summary
 ========
 
-.. todo:: this
+- Operators are top-level "functions", and evaluate to expressions. They are written ``Op(a, b) == expr``, with two equal-signs.
+
+  - Operators can have conditions with ``IF-THEN-ELSE``, and suboperators with ``LET-IN``.
+
+- Sequences are collections of ordered values, and are 1-indexed.
+- Logic is ``/\`` for "and", ``\/`` for "or", and ~ for "not".
+
+  - Logical statements can be written "bullet-points" style.
+
+- Sets are collections of unordered, unique values.
+
+  - We can test if an element is ``\in`` a set or if a set is a ``\subseteq`` of another set.
+  - We can ``\union``, ``\intersect``, and \ (set difference) two sets.
+  - We can CHOOSE elements of sets.
+
+- All types have "sets of" that type. For integers it's ``a..b``, for booleans it's ``BOOLEAN``, for sets it's ``SUBSET``, and for sequences it's ``S1 \X S2``.
+
+  - We can map and filter sets.
 
-- Operators
-- IF
-- sets
-- sequences
-- Map-filter
-- CHOOSE
-- LET
 
 .. [#except-strings] Except strings. Well actually there is a keyword, ``STRING``, but it represents all possible strings, which is an infinitely large set, so...
 .. [#leapsecond] Fun fact, in the original ISO standard seconds could go 1-61! There were *two* leap seconds.