Add temporal logic section

config.toml

@@ -6,4 +6,4 @@ PygmentsCodeFences = true
 
 [Params]
   Author = "Hillel Wayne"
-  menu = ["introduction", "pluscal", "concurrency", "tla", "snippets"]
+  menu = ["introduction", "pluscal", "concurrency", "tla", "temporal-logic"]

content/temporal-logic/index.md

@@ -0,0 +1,10 @@
++++
+title = "Temporal Properties"
+weight = 0
++++
+
+When I said we were barely going to cover TLA+, I wasn't kidding.
+
+[Temporal Properties are the heart and soul of TLA+. It's how the language does _anything_ in the first place. Which is why it's kind of depressing that I'm going to spend almost no time on it. That's because of PlusCal abstracts away most of it for us. This section explains a little bit of the parts we, as startup folk, might find useful.]
+
+[[Editing note: probably doesn't make much sense without the chapter on writing models]]

content/temporal-logic/operators/index.md

@@ -0,0 +1,57 @@
++++
+title = "Temporal Operators"
+weight = 1
++++
+
+## Liveness
+
+Whenever we write invariants, we're saying "for an arbitrary state, this will never happen." And this has been very useful. But there's a trivial system that matches _any_ such case: make sure the initial conditions are correct and then do nothing at all. Safety only tells us something that's true of any moment in any behavior. Sometimes, we want to ask a question about the behavior itself. Most often this is "will this eventually do what we want?" Will the trade eventually happen? Does every thread at some point get priority? Does our algorithm _finish_?
+
+We call these properties "Liveness". And to answer these questions, we use the following new operators.
+
+### []
+
+`[]` is probably the most important operator and the one we're least likely to use. `[]` means _always_: `[]P` means that P is true for all states.
+
+Basically, an invariant. When you put `P` in the invariant box, TLC interprets that as the temporal property `[]P`. The only difference is that TLC is hyper-optimized to handle invariants, so the entire invariants box is basically a convenience thing. So while `[]` implicitly powers all of our invariants, we almost never need to write it explicitly.
+
+### <>
+
+`<>` means _eventually_: `<>P` means that for every possible behavior, at least one state has P as true. For example, the following code is wrong under the temporal property `<>(x = 1)`
+
+```
+(* --algorithm example
+variables x = 3
+begin
+  while x > 0 do
+  with decrement \in {1, 2} do
+    x := x - decrement
+  end with;
+  end while;
+end algorithm; *)
+```
+
+[TODO check this]. There exists one timeline where x never passes through 1: "x = 3 -> x = 2 -> x = 0". So it's not true that 'eventually, x is 1'. As long as every behavior has at least one state satisfying the statement, an eventually is true.
+
+### ~>
+
+`~>` means _leads to_: `P ~> Q` implies that if P ever becomes true, at some point afterwards Q must be true. For example:
+
+```
+(* --algorithm example
+variables x = 4, decrement \in {1, 2}
+begin
+  while x > 0 do
+    x := x - decrement
+  end while;
+end algorithm; *)
+```
+
+As with before, `<>(x = 1)` is not true: we can do `4 -> 2 -> 0`. But the temporal property `(x = 3) ~> (x = 1)` is _true_: there's no way to pass through 3 without also passing through 1.
+
+[adjust this for stuttering]
+
+### <>[]
+
+`<>[]` means _stays as_: `<>[]P` says that at some point P becomes true and then **stays** true. If your program terminates, the final state has to have P as true. [more]
+

content/temporal-logic/unusage/index.md

@@ -0,0 +1,33 @@
++++
+title = "Avoiding Temporal Properties"
+weight = 3
+draft = true
++++
+
+In the last section, we saw a lot of pitfalls of using temporal properties. Perhaps the biggest one is that temporal properties are much, much slower than invariants. Sometimes this is a price you have to pay. Sometimes, though, there are strategies for converting liveness properties into invariants. They aren't perfect, but if you are aware of the problems it can often be worth it.
+
+### []
+
+Use invariants.
+
+### History Flags
+
+Let's assume we want to test `<>P`. If P can only be true in a few monitorable places (for example, it only depends on one variable), we can add a `p_happened = FALSE` variable to our spec, and every time P may have switched to true, add `if P then p_happened := TRUE end if;` to that label. Then, we can express `<>P` as
+
+```
+(\A proc \in ProcSet : pc[proc] = "Done") => p_happened
+```
+
+If you are in the end state, `p_happened` must be true. That's an invariant.
+
+A couple of caveats: This requires a check at _every_ point P can change, otherwise you can potentially have a false error. Also, this only works if you can guarantee that your algorithm terminates; if it does not, then the invariant will never be checked.
+
+A similar technique also works for `P ~> Q`, but it's even jankier.
+
+[note to self, does `/\ P /\ p = FALSE /\ p' = TRUE` work?]
+
+### Termination
+
+asdadsdsa
+
+More stuff definitely

content/temporal-logic/usage/index.md

@@ -0,0 +1,29 @@
++++
+title = "Using Temporal Properties"
+weight = 2
++++
+
+Most often, you're not interested in checking temporal properties. In the cases you are, you can often express what you want through invariants. [Something about ENABLED]. Sometimes, though, you don't have any other option. Here are some things to watch out for.
+
+[[Editing note: this _definitely_ doesn't make sense without the chapter on writing models]]
+
+### Liveness is Slow
+
+It's easy to check that reachable states satisfy invariants. But to check liveness, _how you reach those states_ also matters. If a thousand routes lead through state S, that's 1000 routes that need to be checked for liveness and only one state that needs to be checked for safety. So liveness is intrinsically much, _much_ slower than checking invariants.
+
+### Temporal Properties are Very Slow
+
+The Toolbox has a number of optimizations to make it easier to check invariants: multithreading, model symmetry sets, cloud computing, etc. These all assume, though, that we only care about individual states. None of these apply to temporal properties. So it's even slower to check than you'd think at first.
+
+An especially important one to watch out for are symmetric models. TLC can check them for temporal properties. _However_, the symmetry properties can provide false negatives: it can say that your spec satisfies the properties when it actually doesn't.
+
+### Stuttering and Fairness
+
+TODO
+
+## Recommendations
+
+* Use separate models for invariants and temporal properties.
+* Use smaller sets of model values to check liveness than safety. 
+* Consider testing the same temporal property among several models with different setups.
+* Do not use symmetric model sets.

content/tla/expressions/index.md

@@ -1,93 +1,89 @@
 +++
-title = "Set [Thingy]"
+title = "Expressions"
 weight = 2
-draft = true
 +++
 
-Often, when we have a set of things, we're interested in how those things relate to each other and the set itself. For example, "Given this set of [], are any broken?" Additionally, we often want to choose things out of a set with specific properties, for example "the smallest element". In order to do this, we'll introduce three new set operators. For all these examples, let's assume we've already written the following operator:
+We've been implicitly using _expressions_ up until now; we just haven't clarified them. Doing so it useful, because will help us interview our TLA+ and PlusCal. For our purposes, an expression is __anything that follows a `==`, `=`, `:=`, or `\in`__. All expressions are valid TLA+ and can leverage anything in TLA+. For example, let's say we had the following PlusCal code:
 
-`IsEven(x) == x % 2 = 0`
-
-### \E
-
-`\E` means "exists". We write `\E x \in S : P(x)` to say "there is at least one x in the set such that P(x) is true." If we wanted to check that a set had an even  number in it, we could write `HasEvenNumber(S) == \E x \in S : IsEven(x)`. If there are any even numbers, `HasEvenNumber` is true. Otherwise it's false. Simple.
-
-`~\E` is the opposite: it says that there are no such elements. `\E x \in {}: Foo` is always false, since there are no elements in `{}`.
+[FIXME]
+```
+Foo == 1..10
+(* --algorithm foo
+variables a \in Foo, b = a = 0;
+begin
+  b := CHOOSE x \in Foo : x # a;
+end algorithm; *)
+```
 
-### \A
+[[TODO remove CHOOSE b/c this is now before the section on sets]]
 
-`\A` means "all". We write `\A x \in S : P(x)` to say "For every x in the set,P(x) is true." If we wanted to check that a set had an even number in it, we could write `OnlyEvenNumbers(S) == \A x \in S : IsEven(x)`. If there are only even numbers, `HasEvenNumber` is true. Otherwise it's false. Simple.
+Some things to note here:
 
-`~\A` is the opposite: it says that there is at least one element where P(x) is false. `\A x \in {}: Foo` is always true, since there are no elements in `{}`.
+* In the initial variable setup, we were able to define be a boolean on "is a zero". The first `=` was assignment that started the expression, the second one was an equality check. While you don't need to, it's recommended to wrap the expression here in (), so as to make it clear that the `=` is semantically overloaded.
+* In the algorithm itself, we were able to assign b based on a `CHOOSE` operation. We could just as easily do `b := CHOOSE x \in SUBSET Foo: TRUE` to grab an arbitrary subset.
 
-{{% notice warning %}}
-`\A x \in {}: FALSE` is still true!
+{{% notice tip %}}
+One nice reason to inline `CHOOSE` is to replace a `with`, which can't make procedure calls or use while loops.
 {{% /notice %}}
 
-### CHOOSE
+* A third thing after I make the algorithm better, this is not the editing phase
 
-`CHOOSE` means exactly that. We write `CHOOSE x \in S : P(x)` to say "Throw me whatever x is in S for which P(x) is true". For example, we could write `AnEvenNumber(s) : CHOOSE x \in S : IsEven(x)` to mean "I want an even number." 
+Beyond that, there are ways of increasing the complexity of an expression. Let's examine them.
 
-If there are multiple elements that satisfy the CHOOSE, TLC will create a separate behavior for each element. If there are no elements that satisfy the CHOOSE, TLC will raise an error. That's because there's a problem in your spec. If the set is infinite, TLC will raise an error. That's because TLC can't choose from an infinite sets. There still may be a problem with your spec.
+### LET-IN
 
-## Composing Set Operators
+Any expression can use LET-IN to add local operators and definitions to just that expression alone.
 
-You can specify surprisingly complex properties with just those three additional operators. To demonstrate this, let's burn through some common whiteboard interview problems.
+```
+LET IsEven(x) == x % 2 = 0
+IN  IsEven(5)
 
-_Find the largest element in the set._
+LET IsEven(x) == x % 2 = 0
+    Five == 5
+IN  IsEven(Five)
 
-```
-Max(S) == CHOOSE x \in S : \A y \in S : y <= x
-\* Or
-Max(S) == CHOOSE x \in S : \A y \in S \ {x} : y < x
+LET IsEven(x) == LET Zero == 2
+                 IN  x % Zero = Zero
+    Five == 5
+IN  IsEven(Five)
 ```
 
-"Choose an element of a set where all other elements are smaller than it."
+The whitespace is nonsignificant: we can write `LET IsEven(x) == x % 2 = 0 Five == 5 IN IsEven(Five)` and it will correctly parse it as two separate operators in the LET.
 
-_Here's a list of numbers, do any two add up to N?_
-
-```
-IsTwo(Seq, N) == \E x, y \in 1..Len(Seq) : x # y /\ Seq[x] + Seq[y] = N
-```
+{{% notice info %}}
+Please use newlines. _Please_.
+{{% /notice %}}
 
-"Are there two different numbers that correspond to the points in the sequence that add up to N."
+### IF-THEN-ELSE
 
-_Do any THREE add up to N?_
+C'mon, you know this one.
 
 ```
-IsThree(Seq, N) == \E x, y, z \in 1..Len(Seq) : Cardinality({x, y, z}) = 3 /\ Seq[x] + Seq[y] + Seq[z] = N
+IsEven(x) == IF x % 2 = 0 THEN TRUE
+                          ELSE FALSE
 ```
 
-To make this a little nicer we show that `x # y # z` by saying "If we throw them all into a set, the set should be size three." Otherwise, one of them was a duplicate.
+As before, alignment doesn't matter, but you should align them anyway unless you really hate your coworkers.
 
-_[That annoying stock problem]_
+### CASE 
 
-TODO CLEANUP
+Case is _mostly_ how you'd expect it to act, with one subtle difference.
 
 ```
-BestSell(Prices) == CHOOSE <<min, max>> \in 1..Len(Prices) \X 1..Len(Prices) :
-                      /\ max >= min
-                      /\ \A a, b \in 1..Len(Prices) : 
-                        a <= b 
-                        => Prices[b] - Prices[a] <= Prices[min] - Prices[max]
+CASE x = 1 -> TRUE
+[] x = 2 -> TRUE
+[] x = 3 -> 7
+OTHER -> FALSE
 ```
 
-[Explain]
+OTHER is the default. If none of the cases match and you leave out an OTHER, TLC considers that an error. If _more than one match_, though, you [HIT A BUG IN TLC]
 
-_Given lists of numbers A and B, determine if one is a rotation of the other. Eg 1, 2, 3, 4 is a rotation of 2, 3, 4, 1_
+{{% notice warning %}}
+**THIS IS BROKEN PAGE 298**
+{{% /notice %}}
 
-```
-IsRotation(Seq1, Seq2) == LET len == Len(Seq2)
-                          IN /\ Len(Seq1) = len
-                             /\ \E x \in 1..len :
-                                \A n \in 1..len : Seq1[((n+x)%len)+1] = Seq2[n]
-\* Or
-
-IsRotation(Seq1, Seq2) == LET AllRotations(S) ==
-                              { [ n \in 1..Len(S) |-> S[((n+x)%Len(S))+1]] : x \in 1..Len(S) } 
-                          IN Seq1 \in AllRotations(Seq2)
-```
+## Nesting
 
-"Here's what it means to be a rotation. Does Se1 match that definition?" [Dislike this]
+Of course you can.
 
-[PlusCal Example?]
+[Example]

content/tla/functions/index.md

@@ -1,6 +1,6 @@
 +++
 title = "Functions"
-weight = 3
+weight = 40
 +++
 
 Beyond the basic four types in TLA+ (number, string, boolean, model value), there are two 'complex' types. The first we've already used - that's the set. The other is the function. Functions form the basis of all the 'practical' complex types, so we're going to spend some time on them. Fortunately, the theory is pretty simple.

content/tla/index.md

@@ -5,13 +5,12 @@ weight = 0
 
 Up until now we've been able to model fairly simple systems and discover some subtle bugs in them. We're still fairly limited, however, in what we're able to do. In practical problems we tend to be interested in are far more complicated and require some concepts we can't yet implement. For example, how do you test the invariant "at most one element in the sequence can be a duplicate" or "the largest and smallest element must be within a certain distance of each other"? We don't even have a way yet of specifying "the largest element".
 
-
 For this, we need TLA+.
 
 TLA+ is a mathematical description language. Instead of saying how to find the value you want, you instead say the properties of what you want. For example, the largest element of a set is `CHOOSE x \in S : \A y \in S : y <= x }`. That's not an algorithm. It's just "the number that's bigger than the other numbers."
 
 [A consequence of its descriptiveness is it's possible to build uncheckable models. It's easy, for example, to define the set of all universal turing machines that halt. If you feed that into TLC, though, it will throw an error back. Generally, avoid using infinite sets and you'll probably be fine.]
 
-TLA+ gives us incredible specification power. Not only can we specify complex invariants with it, we can also weave it into our PlusCal code. We can specify per-process flags with `Flags == [pc -> Bool]`. We can []. We can []. PlusCal makes using TLA+ much easier, but TLA+ is what makes PlusCal worthwhile in the first place. Let's get started.
+TLA+ gives us incredible specification power. Not only can we specify complex invariants with it, we can also weave it into our PlusCal code. We can specify per-process flags with `Flags == [pc -> Bool]`. We can []. We can []. PlusCal makes using TLA+ much easier, but TLA+ is what makes PlusCal worthwhile in the first place. The more we understand it, the stronger our PlusCal specifications can be. Let's get started.
 
 Point of note: we're going to be almost completely ignoring the "temporal" part of "Temporal Logic of Actions". As a simple heuristic, we're never, _ever_ going to be talking about "primed and unprimed operators", which make up like 95% of Specifying Systems. At it's core, TLA+ is a beautiful way to elegantly express the temporal properties of a complicated system. For our uses, TLA+ is a way of writing better PlusCal specs. Sacriligious? Probably. Easier? Yup.

content/tla/logical-operators/index.md

@@ -0,0 +1,85 @@
++++
+title = "Logic"
+weight = 30
++++
+
+Introducing logical operators _should_ be a ten-line section, but because there's some wonky indentation rules I'd like emphasize them in detail. **Conjunction and disjunction are the only places in TLA+ where indentation matters.**
+
+### /\ and \/
+
+We've already been using `/\` and `\/`. The former is "and", the latter is "or". `TRUE /\ FALSE = FALSE`, etc.
+
+So, why bring them up again? There's special rules if you want to write a multiline conjugation. What's the value of the following?
+
+```
+TRUE
+\/ TRUE
+/\ FALSE
+```
+
+Trick question, that's an error. TLA+ reads that as `TRUE /\ TRUE \/ FALSE`, which has a precedence issue, so it crashes unless you add parenthesis. You actually have to write it like this:
+
+```
+\/ TRUE
+\/ TRUE
+/\ FALSE
+```
+
+To get `(T \/ T) /\ F`, which is false, or
+
+```
+/\ TRUE
+\/ TRUE
+/\ FALSE
+```
+
+Which is _also_ an error, because you can't alternate operators like that. But we can write
+
+```
+/\ TRUE
+ \/ TRUE
+/\ FALSE
+```
+
+To get `(T \/ T) /\ F`, or 
+
+```
+/\ TRUE
+ \/ TRUE
+ \/ FALSE
+```
+
+To get `(T /\ (T \/ F))`, or
+
+```
+\/ TRUE
+\/ TRUE
+ /\ FALSE
+```
+
+To get `T \/ (T /\ F)`, etc.
+
+Confused at all? No worries if so, since it's pretty confusing. Here's a quick rule of thumb:
+
+* If two logical operators are on the same level of indentation, they are part of the same level of expression.
+* If a logical operator is on a higher level of indentation, it's part of the previous previous operator statement.
+* For comprehensibility's sake, use only one type of operator per level of indentation.
+
+Why is this important to know, versus leaving it all on the same line? Because often you will want to combine simple logic with more complicated expressions. For example, the archetypical definition of the greatest common denominator is
+
+```
+GCD (x,y) ==  CHOOSE gcd \in 1..x:
+                /\ x % gcd = 0
+                /\ y % gcd = 0
+                /\ \A j \in (gcd+1)..x:
+                  \/ x % j # 0
+                  \/ y % j # 0
+```
+
+The gcd divides both x and y, and every number bigger doesn't divide x or doesn't divide y (or both). It's important to have a sense of how the indentation works. FOrtunately, if you make a mistake you're much more likely to get a crash than a bad spec.
+
+## =>
+
+I have no idea where to put this so I'm just throwing it here for the rough draft(s). `=>` is the final logical operator we haven't introduced yet. "P => Q" means "If P is true, then Q must also be true". While it's sometimes useful for expressing properties, it's not necessary: "P => Q" is equivalent to "~P \/ Q", or "Either Q is true or P is false (or both)". If that doesn't seem intuitive to you, take a few minutes to play with it.
+
+[[Stuff on de morgan's laws, etc]]