Fix small issues, add more info on CLI command line options, function…

… ops

docs/core/advanced-operators.rst

@@ -131,7 +131,23 @@ If you `peek <toolbox_misc>` at the definition of the ``Sequences`` module, you'
   set ++ x == set \union {x}
   set -- x == set \ {x}
 
-.. todo:: Function operators
+Function Operators
+==================
+
+This is a bit of syntactic sugar for writing top-level functions:
+
+.. code-block:: tla
+
+  Double == [x \in 1..10 |-> x * 2]
+  
+  \* can also be written as
+
+  Double[x \in 1..10] == x * 2
+
+This is primarily for writing recursive functions::
+
+  Factorial[x \in 0..10] == IF x = 0 THEN 1 ELSE x * Factorial[x - 1]
+
   
 .. index:: CASE
 .. _CASE:

docs/core/functions.rst

@@ -32,6 +32,8 @@ Unsurprisingly, structs are mainly used to represent organized collections of da
 
 Just like sequences, sets, and primitive values, we want some way to generate sets of structs, so we can stick them in our type invariants. Here's how:
 
+.. _struct_set:
+
 ::
 
   \* Accounts is a set of model values
@@ -95,7 +97,7 @@ First of all, throw away the programming definition of "function". The closest t
 
   F == [x \in S |-> expr]
 
-The set we're mapping from, ``S``, is the **domain** of the function, and can be retreived by writing ``DOMAIN F``. That's why we could also use ``DOMAIN`` with sequences and structures:
+The set we're mapping from, ``S``, is the **domain** of the function, and can be retrieved by writing ``DOMAIN F``. That's why we could also use ``DOMAIN`` with sequences and structures:
 
 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.
@@ -232,8 +234,11 @@ You know the drill: new class of value, new need for a way to generate sets of t
 
 The syntax for function sets is ``[S -> T]`` and is "every function where the domain is ``S`` and all of the values are in ``T``." [#codomain]_ In the prior task example, ``assignments`` was always a function in the function set ``[Tasks -> SUBSET CPUs]``.
 
+.. todo:: Explain the function set with a two-stage invariant
+
 .. tip:: A function set of form ``[A -> B]`` will have :math:`\#B^{\#A}` elements in it. If there were two tasks and three CPUs, that would be :math`(2^3)^2 = 64` possible functions.
 
+
   A good way to remember this: ``[1..n -> BOOLEAN]`` is the set of all binary strings of length ``n``, and we know there are :math:`2^n` such strings.
 
 I can also use `set maps <map>` and filters here. Let's say a task can only be assigned to at most two CPUs. If I wanted to, I could fold that into the type invariant, using a function set::

docs/core/modules.rst

@@ -128,6 +128,7 @@ This effectively "rewrites" all of the operators in ``Point`` to use the passed
 .. tip:: If the importing module has a constant with the same name as the child model, it will be imported by default. For example, if both modules contain a ``DEBUG`` constant, the following two are equivalent:
 
   ::
+
     M == INSTANCE Module WITH DEBUG <- DEBUG
     M == INSTANCE Module
 
@@ -138,6 +139,7 @@ This effectively "rewrites" all of the operators in ``Point`` to use the passed
   {content} If you parameterize a module over a variable, you can use actions in that model as regular actions. For example:
 
   ::
+
     ---- MODULE test -----
 
     VARIABLE x

docs/core/operators.rst

@@ -492,7 +492,7 @@ Let's calculate ``ToClock`` the "programming way":
         h_left == seconds % 3600
         m == h_left \div 60
         m_left == h_left % 60
-        s == m_left \div 60
+        s == m_left
       IN
         <<h, m, s>>
 

docs/core/pluscal.rst

@@ -24,6 +24,7 @@ PlusCal
 Let's start with a very simple spec:
 
 .. spec:: pluscal.tla
+
 
 Inside the comment block (``(* *)``) is our PlusCal algorithm. We need to do this because this is a valid TLA+ file; the pluscal algorithm will be compiled to TLA+ below. The algorithm must start with ``--algorithm $name``, otherwise it will be treated like a regular comment. Unlike the module name, the algorithm ``$name`` doesn't need to correspond to anything, and can be your root password for all anyone cares.
 
@@ -390,5 +391,5 @@ Summary of Label Rules
 - While statements must begin with a label.
 - Each variable can only be updated once in a label. (You can assign to multiple parts of a sequence with `|| <||>`.)
 - Macros and ``with`` statements cannot contain labels.
-- A `goto <goto>` must be followed by a new label.
+- A :ref:`goto <goto>` must be followed by a new label.
 - If a branch in a block contains a label inside it, the end of the block must be followed with a label.

docs/examples/index.rst

@@ -68,3 +68,4 @@ PlusCal Specs
 .. todo::
   - ksubsets operator
   - Task ordering
+  - https://tavianator.com/2023/futex.html

docs/examples/partitions.rst

@@ -57,7 +57,8 @@ And that's just a function in the function set ``[{a, b, c} -> 1..3]``! Every fu
   >> PartitionsV1({"a", "b"})
   {<<{}, {"a", "b"}>>, <<{"a"}, {"b"}>>, <<{"b"}, {"a"}>>, <<{"a", "b"}, {}>>}
 
-Now it's just a matter of converting it back to sets. We can do this with a `set map <map>` and a ``Range`` helper. Note that ``Range`` to ``<<{1, 2}, {}>>`` gives us the set ``{{1, 2}, {}}``, which is why we have to set diff out the empty set.
+Now it's just a matter of converting it back to sets. We can do this with a :ref:`set map <map>` and a ``Range`` helper. Note that ``Range`` to ``<<{1, 2}, {}>>`` gives us the set ``{{1, 2}, {}}``, which is why we have to set diff out the empty set.
+
 
 ::
 

docs/index.rst

@@ -41,7 +41,7 @@ This guide is still under development, check :doc:`whatsnew` to see most recent
 About Me
 --------
 
-I'm Hillel. I'm part of the TLA+ foundation and the author of the book `Practical TLA+`_. I wrote this because I want TLA+ to be as accessible as possible and didn't like that my book cost money. I have a `blog`_, a `twitter`_, and a `weekly newsletter`_.
+I'm Hillel. I'm part of the TLA+ foundation and the author of the book `Practical TLA+`_. I wrote this because I want TLA+ to be as accessible as possible and didn't like that my book cost money. I have a `blog`_ and a `weekly newsletter`_.
 
 (Full disclosure, I'm also a `professional  TLA+ consultant <https://hillelwayne.com/consulting/>`__ and <plug>run workshops</plug>.)
 
@@ -84,11 +84,11 @@ I'm Hillel. I'm part of the TLA+ foundation and the author of the book `Practica
 .. _Practical TLA+: https://www.amazon.com/Practical-TLA-Planning-Driven-Development/dp/1484238281
 
 .. _blog: https://www.hillelwayne.com
-.. _twitter: https://twitter.com/hillelogram/
 .. _weekly newsletter: https://buttondown.email/hillelwayne/ 
 
 
 .. http://carefully.understood.systems/blog-2017-04-19-bounded-log-queue.html
 
 .. https://stackoverflow.com/questions/3280712/how-to-allow-certain-threads-to-have-priority-in-locking-a-mutex-use-pthreads
 
+.. todolist:: 

docs/intro/conceptual-overview.rst

@@ -4,9 +4,6 @@
 Conceptual Overview
 +++++++++++++++++++
 
-
-.. todo:: Mention the name TLC
-
 To justify the value of TLA+, let's talk about how it's useful, and how it's different from programming languages.
 
 Imagine we're building a wire transfer service for a bank. Users can make transfers to other users. As a requirement, we don't allow any wires that would overdraft the user's account, or make it go below zero dollars. At a high level, the could would look like this:

docs/reference/standard-library.rst

@@ -126,6 +126,9 @@ BagCardinality(bag)
 CopiesIn(e, bag)
   If ``e`` is in ``bag``, then ``bag[e]``, otherwise 0.
 
+
+.. _tlc_module:
+
 TLC
 ============
 
@@ -165,6 +168,9 @@ Print(val, out)
 PrintT(val)
   Equivalent to ``Print(val, TRUE)``.
 
+Any
+  ``x \in Any`` for *any* value ``x``. Don't use this as part of a ``Spec``, but it's occasionally useful for modeling properties.
+
 Assert(bool, errmsg)
   If ``bool`` is false, then terminates model checking with ``errmsg``. Otherwise, evaluates to TRUE.
 
@@ -174,6 +180,9 @@ RandomElement(set)
 TLCEval(v)
   Evaluates the expression ``v`` and caches the result. Can be used to speed up recursive definitions.
 
+
+.. _tlcget:
+
 TLCGet(val)
   val can be either an integer or a string. If an integer, retrieves the value from the corresponding TLCSet. If a string, retrieves statistics from the current model run. The following strings are valid:
 

docs/topics/cli.rst

@@ -26,7 +26,7 @@ This will:
 
 1. Translate the text *in file* to TLA+
 2. Write ``file.old`` as a backup
-3. Write ``file.cfg`` as a `configuration file <cfg>`, overwriting it if it already exists.
+3. Write ``file.cfg`` as a :ref:`configuration file <cfg>`, overwriting it if it already exists.
 
 To prevent (3), add ``-nocfg`` as a flag before ``file.tla``. There is no way to prevent the translator from writing ``file.old``. I have a shell watcher that finds and deletes them.
 
@@ -139,5 +139,14 @@ Now that we know how to run a config file, let's get back to the TLC options. Yo
 
   You can also write ``-dump dot,colorize file`` to color the edges based on the actions they involve and ``-dump dot,actionlabels`` to label the edges with the corresponding action. Both can be used together.
 
-``metadir dir``
+``-metadir dir``
   Instead of storing the seen statespace in the same directory as the spec, TLC will instead store it in ``dir``. I find this useful when scripting against the CLI, as I can store the state space in a temporary directory for easier cleanup.
+
+``-workers num/auto``
+  Specifies the number of worker threads to use for model checking. **This is very important.** Without this, the CLI defaults to a single worker. Pass in ``auto`` to use as many workers as you have cores.
+
+``-noGenerateSpecTE``
+  Newer versions of TLA+ save an error file whenever it finds a property error. This flag disables writing the file.
+
+``-fpmem num``
+  What percentage of the system memory to earmark for model checking, expressed as a decimal. Defaults to ``0.25`` (1/4 the memory).

docs/topics/index.rst

@@ -15,11 +15,11 @@ This is a collection of techniques and essays on using TLA+ more effectively. Pe
   toolbox
   cli
   aux-vars
-  state-machines
   refinement
 
 .. toctree::
   :caption: How to Model...
   :maxdepth: 1
 
   Message Queues <message-queues>
+  state-machines

docs/topics/toolbox.rst

@@ -100,7 +100,7 @@ State Constraint
 
   Liveness invariants can't be checked when the state constraint is active.
 
-  .. tip:: State constraints are a good way to bound unbound models.
+  .. tip:: State constraints are a good way to bound :ref:`unbound models <topic_unbound_models>`.
 
 Action Constraint