Another grand of words + screenshots

docs/beginner/action-properties.rst

@@ -79,6 +79,9 @@ On one hand, cool trick. On the other, we now have to figure out what ``[][count
 
 It's finally time to talk about the "actions" in "Temporal Logic of Actions".
 
+.. index:: ' (next value)
+.. _prime:
+
 So remember how way back I said that `strings must use double quotes <string>`? That's because single quotes have a special role in TLA+! In any given step, ``x'`` is the value of x at the *end of the step*, and what it starts as in the *next* step. ``[](x' >= x)``, then, is "it is always true that the *next value of x* is larger than x".
 
 .. tip:: you can use primed operators in the `trace explorer`. It'll show you the value of the expression in the next step.

docs/beginner/advanced-operators.rst

@@ -8,9 +8,9 @@ This isn't much more complicated than the last sections, but this is the best pl
 
 Sum up sequence.
 
-I mean sure, we can write a Pluscal algoirhtm to do that:
+I mean sure, we can write a Pluscal algoirthm to do that:
 
-.. todo:: <alg>
+.. spec:: advanced_operators/sum.tla
 
 But how the heck do you write ``SumSeq``?!
 
@@ -89,7 +89,7 @@ Not too bad. You can define anonymous operators with ``LAMBDA``:
 Binary operators
 ================
 
-If you `peek <toolbox_misc>` at the definition of the `Sequences` module, you'll see how it defines ``\o``:
+If you `peek <toolbox_misc>` at the definition of the ``Sequences`` module, you'll see how it defines ``\o``:
 
 ::
 

docs/beginner/index.rst

@@ -6,8 +6,13 @@ Core
 
 This is the core language material. You can think of this section as a self-contained "book" that gets you from a complete outsider to a beginning practitioner. People who are already comfortable with TLA+ may find the :doc:`topics </topics/index>` more useful.
 
-.. who this is for
-.. who this is not for
+.. todo::
+
+  who this is for
+
+  who this is not for
+
+  mention TLC, unbound models
 
 Outline
 ========

docs/beginner/invariants.rst

@@ -46,11 +46,11 @@ This operator needs to know about the ``all_unique`` variable, so we have to put
 
 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:: {SCREENSHOT}
+.. figure:: SCREENSHOT
 
-.. todo:: {CONTENT} talk about the error trace
+This shows a series of steps, starting from the initial state. Let's look at the first two states in more detail. {CONTENT} talk about the error trace
 
-  (There's a little more we can do with the error trace, see `here <topic_toolbox>`.)
+  (There's a little more we can do with the error trace, see :doc:`here </topic/toolbox>`.)
 
 
 So back to the nature of the invariant. We say ``all_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:
@@ -125,6 +125,18 @@ On every label *except* "Done", this evaluates to TRUE and the invariant passes.
 
 I said ``=>`` was really important earlier. This is one of those ways: it lets us say invariants should only apply under certain conditions. 
 
+.. warning::
+
+  ``=>`` follows the same indentation rules as other boolean operators. This means that
+
+  ::
+
+    /\ A
+    /\ B
+     => C
+
+  Is interpreted as ``A /\ (B => C)``, *not* ``(A /\ B) => C``. When it doubt, add in parenthesis.
+
 We can now run this as our full invariant, and the spec works :ss:`duplicates_many_inputs`. 
 
 .. index::
@@ -344,13 +356,13 @@ This now passes.
 
   .. rubric:: More invariant practice
 
-    _issorted:
+  _issorted:
 
-    ::
+  ::
 
-      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]
 
   .. todo:: Find actual names for everything
 

docs/beginner/pluscal.rst

@@ -10,8 +10,7 @@ Overview
 
 In the :doc:`last chapter <operators>`, we introduced operators, sets, and values, and did some simple computation with them. Now that we have that groundwork done, it's time to actually talk about specifications.
 
-.. index:: PlusCal
-  :name: pluscal
+.. index:: pluscal
 
 TLA+ is the *Temporal Logic of Actions*, where the "actions" are descriptions of state changes in the system. It's a powerful way of expressing mutation, but it is also very general, accepting a large degree of complexity to be able to express more powerful systems. Many engineers struggle to start learning it. So in 2009, Leslie Lamport created a DSL called PlusCal: a more programming-like syntax that compiles to TLA+ actions.
 
@@ -46,6 +45,8 @@ Alternatively, we can use :kbd:`cmd-T` on Mac or :kbd:`ctrl-T` on Windows and Li
 
 That's what's actually run when we model check this spec.
 
+.. tip:: If you right-click in the spec, there's an option at the bottom of the context menu to "Translate PlusCal Automatically". This helps if you keep forgetting to translate, though it raises an error if you're writing a :doc:`pure TLA+ spec <tla>`.
+
 .. index:: Labels
   :name: label
 
@@ -102,7 +103,7 @@ The point is this: the labels let us specify just how concurrent our system is.
 Label Rules
 --------------
 
-We're modeling time here, so there are restrictions on where we can place the labels.
+We're modeling time here, so there are restrictions on where we can place the labels. We'll recap all of the label rules `at the end <label_rules_summary>`.
 
 First, **all statements must belong to a label.** This means, among other things, that you miust always start the algorithm with a label.
 
@@ -131,11 +132,16 @@ PlusCal expressions
 
 In addition to updates, there are three other statement-level constructs: 
 
-.. index:: skip; assert; goto
+.. index:: skip, assert, goto
 .. _goto:
 
 * ``skip``: a noop.
 * ``assert expr``: TLC immediately fails the model check if ``expr`` is false. (This breaks the "everything in the label happens at once", as TLC will stop *as soon* as it finds a failing ``assert``.) To use ``assert`` you need to extend ``TLC``.
+
+  .. warning::
+
+    The error trace will *not* show the step that triggered the failing assert! For that reason, prefer invariants to asserts.
+
 * ``goto L``: jumps to label ``L``. **A label must immediately follow any goto statement**.
 
 .. todo:: {CONTENT} Also mention print
@@ -236,8 +242,6 @@ while
 
 **While is nonatomic**. After each iteration of the while loop, we're back at the ``Sum`` label. Other processes can run before the next iteration. This doesn't change things for single process algorithms, but it will matter a lot when we start adding in concurrency.
 
-.. todo:: {exercise}  showing that it has multiple states
-
 .. index:: ! duplicates
 .. _duplicates:
 
@@ -348,6 +352,8 @@ Summary
   - ``with`` creates temporary identifiers in a block.
   - ``while`` statements are nonatomic: every loop happens in a separate step.
 
+.. _label_rules_summary:
+
 Summary of Label Rules
 ----------------------
 
@@ -357,20 +363,3 @@ Summary of Label Rules
 - Macros and ``with`` statements cannot contain labels.
 - A `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.
-
-- PlusCal expressions:
-
-  - assert, goto, skip
-
-- PlusCal constructs
-
-  - If
-  - While
-  - Macro
-  - With
-
-
-- Labels represent *atomicity*.
-
-  - Label rules:
-

docs/data.yml

@@ -90,6 +90,5 @@ state_spaces:
     distinct: 17
     states: 19
   wire_overview:
-    config: 1
-    distinct: 1
-    states: 2
+    distinct: 518794
+    states: 835594

docs/examples/index.rst

@@ -43,3 +43,10 @@ PlusCal Specs
 
   https://andy.hammerhartes.de/finding-bugs-in-systems-through-formalization.html
 
+  https://www.g9labs.com/2022/03/12/what-s-the-fuss-about-formal-specifications-part-2/
+
+.. todo::
+
+  Ideas:
+
+    - Mutex DAG tracer?

docs/intro/conceptual-overview.rst

@@ -59,6 +59,12 @@ The specification has a set of "behaviors", or possible distinct executions. For
 
 .. todo:: {GRAPH}
 
+  .. digraph:: G
+
+    node[label=""]
+
+    A -> B -> C;
+
   Each box is a state. Any sequence of boxes and arrows is a behavior. The set of all behaviors forms the specification.
 
 .. note:: "No account can overdraft" is an **invariant** property, which is one that must be true of every single state of every single behavior. There are other, more advanced properties, like `liveness <chapter_temporal_logic>` and `action <chapter_action_properties>` properties, which we'll cover in time.
@@ -77,7 +83,7 @@ Specifications
 
 So what does this all look like in practice? Let's present a spec for wire transfers, first with hardcoded parameters and then with model-parameterizable ones.
 
-.. spec:: wire.tla
+.. spec:: wire/1/wire.tla
   :name: wire
   :fails:
 
@@ -89,7 +95,7 @@ Over the rest of the book I'll be covering how all of this works syntactically.
 * The variable ``acct`` isn't a fixed value, it is one of 100 different values, one for each element of ``[People -> Money]``. When we model check this, TLC will explore every possible behavior starting from every one of these 100 possible initial values.
 * ``NoOverdrafts`` is a `quantifier <\A>`. It's true if *every* account is >= 0 and false otherwise. In python, this might be equivalent to ``all([acct[p] >= 0 for p in People])``. Quantifiers are an extremely powerful feature of TLA+, making it easy to write very complex properties.
 * We have more than one ``wire`` `process` running simultaneously. With ``NumTransfers == 2``, there are two processes in the spec. But we can choose to have ten, a hundred, or a thousand processes if we really want, our only limit is our CPU time.
-* Each step of the algorithm belongs to a separate `label`. The labels determine what happens atomically and what can be interrupted by another process. That way we can represent race conditions.
+* Each step of the algorithm belongs to a separate `label <label>`. The labels determine what happens atomically and what can be interrupted by another process. That way we can represent race conditions.
 
 
 Models
@@ -101,16 +107,13 @@ Once we have our design, we can model check it against some requirements. We can
 
 We checked it with two transfers. But what if we wanted to check it with four transfers? TLA+ makes it very easy to change our designs. We can parameterize any value, and then have different models check with different values.
 
-.. todo:: wire2
-
-.. spec:: wire.tla
+.. spec:: wire/2/wire.tla
+  :diff: wire/1/wire.tla
   :fails:
 
-Now I can make separate models, with the same invariant, but different numbers of workers.
+Now I can make separate models, with the same invariant, but different numbers of simultaneous transfers. So I can see that it works correctly with one transfer but not two. 
 
 Discussion
 ==========
 
 There's a few concepts I haven't introduced here: temporal properties, fairness, stutter-invariance, etc. All of these will be covered later. Hopefully, though, this is enough to give you a sense of what, if you decide to learn TLA+, you'll actually be able to *do* with it. If you're interested in continuing, check out the :doc:`core </beginner/index>` and `setup`.
-
-Test with the fixed 

docs/specs/advanced_operators/sum.tla

@@ -0,0 +1,33 @@
+---- MODULE sum ----
+EXTENDS Integers, Sequences, TLC, FiniteSets
+CONSTANT S
+ASSUME S \subseteq Int
+
+SumSeq(s) == 0 \* ???
+
+(*--algorithm dup
+variable 
+  seq \in [1..5 -> S];
+  sum = 0;
+  i = 1;
+
+define
+  TypeInvariant ==
+    /\ sum \in Int
+    /\ i \in 1..Len(seq)+1
+
+  IsCorrect == pc = "Done" => sum = SumSeq(seq)
+end define; 
+
+macro add(x, val) begin
+  x := x + val
+end macro;
+
+begin
+  Iterate:
+    while i <= Len(seq) do
+      add(sum, seq[i]);
+      add(i, 1);
+    end while;
+end algorithm; *)
+====

docs/specs/topics/trace.tla

@@ -0,0 +1,34 @@
+---- MODULE trace ----
+
+EXTENDS Integers, TLC
+
+(*--algorithm errortrace
+variable x=0; y=0; i=0;
+
+define
+  xyleq10 == x * y <= 10
+end define;
+
+process incX = "incX"
+begin
+  EtX:
+    while i < 8 do
+      x := x + 1;
+      i := i + 1;
+    end while;
+end process;
+
+process incY = "incY"
+begin
+  EtY:
+    while i < 8 do
+      y := y + 1;
+      i := i + 1;
+    end while;
+end process;
+
+end algorithm; *)
+
+
+====
+

docs/specs/wire.tla → docs/specs/wire/1/wire.tla

@@ -3,7 +3,9 @@ EXTENDS TLC, Integers
 
 People == {"alice", "bob"}
 Money == 1..10
-(*--algorithm wire
+NumTransfers == 2
+
+(* --algorithm wire
 variables
   acct \in [People -> Money];
 
@@ -13,11 +15,11 @@ define
       acct[p] >= 0
 end define;
 
-process wire \in {1, 2}
+process wire \in 1..NumTransfers
 variable
-amnt \in 1..5;
-from \in People;
-to \in People
+  amnt \in 1..5;
+  from \in People;
+  to \in People
 begin
   Check:
     if acct[from] >= amnt then

docs/specs/wire/2/wire.tla

@@ -0,0 +1,31 @@
+---- MODULE wire ----
+EXTENDS TLC, Integers
+CONSTANTS People, Money, NumTransfers
+
+(* --algorithm wire
+variables
+  acct \in [People -> Money];
+
+define
+  NoOverdrafts ==
+    \A p \in People:
+      acct[p] >= 0
+end define;
+
+process wire \in 1..NumTransfers
+variable
+  amnt \in 1..5;
+  from \in People;
+  to \in People
+begin
+  Check:
+    if acct[from] >= amnt then
+      Withdraw:
+        acct[from] := acct[from] - amnt;
+      Deposit:
+        acct[to] := acct[to] + amnt;
+    end if;
+end process;
+end algorithm; *)
+
+====