Changes all around

pretentious7 · Jun 27, 2022 · 569aa35 · 569aa35
1 parent 5d0372d
commit 569aa35
Show file tree

Hide file tree

Showing 12 changed files with 178 additions and 59 deletions.
diff --git a/docs/core/index.rst b/docs/core/index.rst
@@ -10,7 +10,9 @@ This is the core language material. You can think of this section as a self-cont
 
   who this is for
 
-  who this is not for
+  who this is not for:
+    - beginners
+    - people who want to verify code directly
 
   mention TLC, unbound models
 

diff --git a/docs/core/next-steps.rst b/docs/core/next-steps.rst
@@ -4,4 +4,10 @@
 Next Steps
 ++++++++++++++++++++++
 
-Congratulations! You've reached the end of the core. You're now fully qualified to write any kind of TLA+ spec.
+Congratulations! You've reached the end of the core. You're now a TLA+ expert.
+
+:doc:`topics </topics/index>`
+
+:doc:`examples </examples/index>`
+Read topics
+Examples
diff --git a/docs/examples/index.rst b/docs/examples/index.rst
@@ -1,4 +1,25 @@
-.. note:: There aren't a whole lot of examples uploaded yet. I'll be writing more as I continue to work on the site.
+.. note:: There aren't a whole lot of examples uploaded yet. I'll be writing more as I continue to work on the site. In the meantime, here are some good examples from around the web!
+
+  * `TLA+ Example Repository <https://github.com/tlaplus/Examples>`__: The official repo, mostly abstract algorithms and protocols.
+
+  * `Modeling a message passing bug with TLA <https://medium.com/@polyglot_factotum/modelling-a-message-passing-bug-with-tla-baaf090a688d>`__
+
+  * `The Tortoise and Hare in TLA+ <https://surfingcomplexity.blog/2017/10/16/the-tortoise-and-the-hare-in-tla/>`__: That finding cycles in a linked list algorithm question, formally modeled.
+
+  * `Message Queues <https://www.hillelwayne.com/post/tla-messages/>`__: Pubsub implementations with topics readers subscribe to.
+
+  * `Thread Bounded Queue <https://www.hillelwayne.com/post/augmenting-agile/>`__: finding a deadlock in a bounded queue, where writers trying to write a full queue are temporarily put to sleep.
+
+  * `Adversarial Modeling <https://www.hillelwayne.com/post/adversaries/>`__: A short example of splitting a spec into "machine" and "world" components, where the world acts as an adversary against the machine.
+
+  * `Xen VChan <http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/>`__
+
+  * `Batch uploader <https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f>`__: The first spec I wrote in production!
+
+  * `Process Handler <https://andy.hammerhartes.de/finding-bugs-in-systems-through-formalization.html>`__
+
+  * `Payment Handler <https://www.g9labs.com/2022/03/12/what-s-the-fuss-about-formal-specifications-part-2/>`__: Like the wire example in the conceptual overview, except in real life.
+
 
 +++++++++
 Operators
@@ -24,27 +45,7 @@ PlusCal Specs
 
 .. todo:: 
 
-  https://medium.com/@polyglot_factotum/modelling-a-message-passing-bug-with-tla-baaf090a688d
-
-  https://surfingcomplexity.blog/2017/10/16/the-tortoise-and-the-hare-in-tla/
-
-  https://www.hillelwayne.com/post/tla-messages/
-
-  https://www.hillelwayne.com/post/augmenting-agile/
-
-  https://www.hillelwayne.com/post/adversaries/
-
-  https://github.com/tlaplus/Examples
-
-  http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/
-
-
-  https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f
-
-  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:

diff --git a/docs/index.rst b/docs/index.rst
@@ -9,39 +9,41 @@
 
 .. note::
 
-  Welcome to Learn TLA+! This is still a work in progress, please see :doc:`whatsnew` for updates and please raise any questions or concerns at the `github repo <https://github.com/hwayne/learntla-v2>`__.
+  Welcome to Learn TLA+! This is still a work in progress, please see :doc:`whatsnew` for updates and please raise any questions or concerns at the `github repo <https://github.com/hwayne/learntla-v2>`__. I'd love to hear your feedback!
 
   (In the meantime, you can find the old version at `old.learntla.com <https://old.learntla.com>`__.)
 
-Learn TLA+
+Learn TLA+ and Debug your Designs
 ====================================
 
-Most software flaws come from one of two places. A code bug is when the code doesn't match our design— for example, an off-by-one error, or a null derefence. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, the best most of us are taught is "think about it really hard".
+Most software flaws come from one of two places. A code bug is when the code doesn't match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we're just taught to "think about it really hard".
 
-TLA+ is a language for design systems that lets you directly test those designs. Think of it like making an outline of what you want to build, and then finding erros in the outline.  and then directly test those designs. 
+TLA+ is a "formal specification language", a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and Crowdstrike. Think of it like making an outline of what you want to build and then finding errors in the outline itself. 
 
-`genindex`
+TLA+ doesn't replace our engineering skill but *augments* it. With TLA+ we can design systems faster and more confidently. When I first discovered it, it saved my company weeks of work and hundreds of thousands of dollars annually. Since then, I've wanted to make it as accessible as possible to as many people as possible. 
+
+.. todo:: Better intro
 
 About this guide
 ----------------
 
 This is a free online resource for learning TLA+. To help both beginners and experienced users, the guide is divided into three parts:
 
-- The *core*: a linear introduction to all of the TLA+ language. It starts with basic operators and gradually progresses all the way to advanced topics. The core is intended to be read **linearly**: people new to TLA+ should start with the conceptual overview, and then work forward from there. People comfortable with TLA+ should skim until they find the new material.
+- The *Core*: a linear introduction to all of the TLA+ language. It starts with basic operators and gradually progresses all the way to advanced topics. The core is intended to be read **linearly**: people new to TLA+ should start with the conceptual overview and then work forward from there. People comfortable with TLA+ should skim until they find new material.
 
 - *Topics*: "Optional" advanced material. Any individual lesson will be useful to *many* but not *all* TLA+ users. Unlike the core, these are designed to be mostly independent of each other. If topics have dependencies on other topics, I will call them out.
 
 - *Examples:* Applications of TLA+ to specs, showing both how to write and understand specs. 
 
-The guide is still under development, check :doc:`whatsnew` to see most recent updates and the `roadmap <roadmap>` to see what I'm currently working on.
+This guide is still under development, check :doc:`whatsnew` to see most recent updates and the `roadmap <roadmap>` to see what I'm currently working on.
 
 
-About me
+About Me
 --------
 
-I'm Hillel. I created a `previous version <old.learntla.com>`__ of *Learn TLA+* and am the author of the book `Practical TLA+`_. I wrote this because I was unsatisfied with the previous version of the website and didn't like how seeing the best resource on TLA+ wasn't free. 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`_, a `twitter`_, and a `weekly newsletter`_.
 
-.. todo:: TLA+ vs pluscal page with prerequisites
+.. I also maintain the `Alloy documentation <https://alloy.readthedocs.io/en/latest/>`__ and have a strong interest in `software history <https://www.hillelwayne.com/post/linked-lists/>`__, `software engineering culture <https://www.hillelwayne.com/post/are-we-really-engineers/>`__
 
 .. toctree::
   :maxdepth: 2
@@ -74,12 +76,11 @@ I'm Hillel. I created a `previous version <old.learntla.com>`__ of *Learn TLA+*
   reference/other-resources
 
 .. todo:: https://stackoverflow.com/questions/25243482/how-to-add-sphinx-generated-index-to-the-sidebar-when-using-read-the-docs-theme
-
+
+.. todo:: TLA+ compared to other formal methods
 
 .. todolist::
 
-.. todo:: == vs =
-
 
 .. _Practical TLA+: https://www.amazon.com/Practical-TLA-Planning-Driven-Development/dp/1484238281
 

diff --git a/docs/intro/faq.rst b/docs/intro/faq.rst
@@ -0,0 +1,35 @@
+:orphan:
+
+##############
+Intro FAQ
+##############
+
+Who is TLA+ For?
+=================
+
+It's awesome!
+
+What can't TLA+ do?
+====================
+
+Test code directly
+numbers
+String manipulation
+Probabilistic properties
+Good layouts
+
+
+I've got my design working, but how do I know my code is correct?
+================================================================
+
+Can't easily
+Generate tests from sync
+
+How does it compare to ${OTHER_LANGUAGE}
+========================================
+
+I haven't written this yet but plan to.
+
+How does it compare to testing?
+
+How does it compare to property-based testing?
diff --git a/docs/reference/glossary.rst b/docs/reference/glossary.rst
@@ -14,18 +14,55 @@ Term Guide
     The name of the model checker for TLA+. The site uses "TLC" and "model checker" interchangeably.
 
   PlusCal
-    TODO
+    A DSL for writing TLA+ algorithms.
 
   TLA+
-    The "Temporal Logic of Actions". A :term:`formal specification language`
+    The "Temporal Logic of Actions", used for modeling concurrent systems. A :term:`formal specification language`. You can either write in TLA+ directly or use the :term:`PlusCal` DSL.
 
 
   Formal Specification Language
-    TODO
+    A language you use to describe a system you're building, so you can find errors in it.
 
   Formal Methods
     The discipline of writing rigorous, verified code.
 
+  Safety
+    A property that a bad thing *doesn't* happen. Most (but not all) safety properties are invariants. All invariants are safety properties.
+
+  Liveness
+    A property that a good thing *is guaranteed* to happen. All liveness properties are temporal properties.
+
+  Invariant
+    Something that must be true at every state in the system. All invariants are safety properties.
+
+  Property
+    Something we want to be true of the system. All properties in TLA+ can be broken into safety and liveness properties.
+
+  Temporal Property
+    A property that spans more than one state. For example, "the counter must never decrease" or 
+
+  Predicate
+    A boolean expression.
+
+  Behavior
+    A sequence of states, or "timeline", in the system.
+
+  State space
+    The set of all possible states reachable by all possible behaviors in a model.
+
+  TLA+ Toolbox
+    The official TLA+ IDE.
+
+..
+
+  State space explosion
+  Quantifier
+  Model
+  Spec
+  Module
+  Model Checking
+  Machine
+  World
 
 Symbol Guide
 ============

diff --git a/docs/reference/other-resources.rst b/docs/reference/other-resources.rst
@@ -2,4 +2,22 @@
 Other Resources
 ++++++++++++++++++++++
 
-TODO
+Learning Resources
+==================
+
+.. todo:: This
+
+Apalache
+
+old.learntla
+
+Specifying systems
+
+Model book
+
+Pragmatic modeling
+
+Reading Resources
+=================
+
+http://glat.info/pdf/formal-methods-amazon-2014-11.pdf
diff --git a/docs/topics/aux-vars.rst b/docs/topics/aux-vars.rst
@@ -39,8 +39,7 @@ Variables that represent something that happened. ``Q_was_true`` is a history va
 You can also use history variables to track past information no longer present in the system. For example, say you have clients querying a database, which can be updated in the middle in the request. You could add a variable called ``aux_client_request_value`` that is updated *as soon as the client makes the request*, so that updating the database value doesn't lose the information about what the value was at the time of the request.
 
 
-.. message pool, seen messages
-.. todo:: Pull the example from Dekker
+.. todo:: message pool, seen messages
 
 .. tip:: As a rule of thumb, the spec behavior should not depend on a history variable. If it does, then it's state information the machine you're making has access to, so should be lifted from an auxiliary variable to a real one.
 
@@ -136,9 +135,9 @@ Prophecy variables dictate something will happen *in the future*. Effectively th
 Usage Notes
 ===============
 
-Don't make the code use them
+When using aux vars, you should make it clear what are "machine" variables that are part of the system and what are auxiliary variables that aren't part of it. If you can't implement something then your spec shouldn't depend on it!
 
-Aux vars are tricky to use in raw TLA+, as they need to be included in ``UNCHANGED`` statements.  You can use sequences to help with this. 
+Aux vars can be fiddly in raw TLA+, as they need to be included in ``UNCHANGED`` statements.  You can use sequences to help with this. 
 
 
 
diff --git a/docs/topics/cli.rst b/docs/topics/cli.rst
@@ -9,7 +9,7 @@ Most people use the Toolbox for TLA+. But you can also use `vscode <https://mark
 The Command Line
 =================
 
-The main CLI file is ``tla2tools.jar``. You can download it directly from `this link <https://github.com/tlaplus/tlaplus/releases>`_. You can also find it in the Toolbox installation, in the base directory.
+The main CLI file is ``tla2tools.jar``. You can download it directly from `this link <https://github.com/tlaplus/tlaplus/releases>`_. You can also find it in the base directory of your toolbox installation.
 
 Tlatools has four subtools: TLC, the pluscal translator, a latex pdf generator (Tla2Tex), and a parser (SANY). I'll leave documenting the latter two tools to `Lamport <https://lamport.azurewebsites.net/tla/current-tools.pdf>`_ and focus on the translator and model checker.
 

diff --git a/docs/topics/state-machines.rst b/docs/topics/state-machines.rst
@@ -73,6 +73,12 @@ What's better than a state machine? A *nested* state machine.
 
 Also known as `Harel Statecharts <https://www.cs.scranton.edu/~mccloske/courses/se507/harel_Statecharts.pdf>`__, hierarchical state machines allow states inside of other states. If state P' is inside of state P, then P' can take any transitions that P can take. A simple example is the UI of a web app. You can log on or off, and when logged in you start in a homepage and can move to any secondary page. To make things interesting we'll say one of the secondary pages also as subpages.
 
+.. note:: There's a few different flavors of HSM. For this one, I'm following three restrictions:
+
+  1. Transitions can start from any state, but must end in a "leaf" state. You can't be in ``LoggedIn`` or ``Reports``, you have to be in ``Main`` or ``Report1``.
+  2. A state can't have two different parent states.
+  3. No state cycles.
+
 .. todo:: Graphviz Group
 .. digraph:: hsl
 
@@ -98,15 +104,20 @@ Also known as `Harel Statecharts <https://www.cs.scranton.edu/~mccloske/courses/
   }
   Main -> LogOut[ltail="cluster_app"];
 
-There's a few different flavors of HSM. For this one, I'm following three restrictions:
+To model the hierarchical states, I want to be able to write ``Trans("LoggedIn", "Logout")`` and have that include every state of the app: Main, Settings, Report1, and Report2. So we need an ``In(state1, state2)`` that's recursive. Then ``Trans`` becomes
 
-1. Transitions can start from any state, but must end in a "leaf" state. You can't be in ``LoggedIn`` or ``Reports``, you have to be in ``Main`` or ``Report1``.
-2. A state can't have two different parent states.
-3. No cycles.
+::
 
+  Trans(from, to) ==
+    ...
 
+To represent the state hierarchy, we can go either top-down (a function from states to the set of child states) or bottom-up (a function from states to their parent states). Each has relative tradeoffs:
 
-1. *Function from states to their parents*: Impossible for a state to have two parents. Worse ergonomics on checking transitive membership, as not all states will be in the function domain.
-2. *Function from states to the set of children*: Function domain guaranteed to be all states. Two states can have the same child state.
+#. *Top-down*: Function domain guaranteed to be all states. Can accidentally give two states the same child.
+#. *Bottom-up*: Impossible for a state to have two parents. Worse ergonomics on checking ``In``, as not all states will be in the function's domain. Harder to check if a state doesn't have children.
 
 Ah heck, let's implement both and check they're equivalent.
+
+.. todo:: code
+
+  . Let's prove the two are equivalent!
diff --git a/docs/topics/tips.rst b/docs/topics/tips.rst
@@ -12,7 +12,6 @@ General small things for writing better specs.
 Both TLA+ and PlusCal
 ======================
 
-.. todo:: Tagged unions
 
 Use ASSUME
 -----------
@@ -29,10 +28,20 @@ From this it's clear that Threads is a set and NULL is not a thread.
 
 .. todo:: Using ASSUME for operators
 
-Use LET to Simplify Operators
------------------------------
 
-.. todo:: {CONTENT}
+.. todo:: {CONTENT} Use LET to Simplify Operators
+
+Model tagged unions with structs
+-------------------------------------------
+
+TLC can't have a set of strings and integers. If you need that, you can instead use structs with a ``type`` and ``val`` field.
+
+::
+
+  {
+   [type |-> "int", val |-> 1], 
+   [type |-> "str", val |-> "1"] \* ok
+  }
 
 Decompose functions of structs
 ------------------------------
@@ -78,7 +87,6 @@ In general, I mostly use structures for immutable values, like the bodies of mes
 Separate Safety and Liveness Models
 -------------------------------------
 
-
 .. todo:: {CONTENT} more on model optimization
 
 Since liveness properties take a lot longer to check (and can't use `symmetry sets <symmetry_set>`), I use a separate model for just checking liveness properties, which uses smaller constants.

diff --git a/docs/topics/toolbox.rst b/docs/topics/toolbox.rst
@@ -164,8 +164,9 @@ TLC command-line parameters
 Misc Features
 ================
 
-- There's autocomplete with ``ctrl+space``.
-- Pressing ``F3`` on a module name will jump to its definition.  
+- ``ctrl+space`` will start autocompletion.
+- Pressing ``F3`` on a module name will jump to its definition.
+- In the right click menu, there's an option to "translate pluscal automatically", which translates the spec on every save. This will raise an error if your spec isn't pluscal, though.
 
 .. _graphviz: https://graphviz.org/