Merge pull request #2825 from fan-tom/fix-docs

Fix various issues in docs

docs/README.md

@@ -3,7 +3,7 @@
 The Apalache documentation is written in markdown files in the [./src](./src)
 directory and compiled using [mdbook](https://github.com/rust-lang/mdBook).
 
-To view the documentation, visit https://apalache.informal.systems/docs/ .
+To view the documentation, visit https://apalache.informal.systems/docs/.
 
 ## Building and previewing the documentation
 
@@ -41,7 +41,7 @@ Our CI uses the [emojitsu](https://github.com/shonfeder/emojitsu#emojitsu) CLI
 utility. You can also use this tool to lookup the name for an emoji if you have
 the unicode on hand or to see how a name will render.
 
-Note that GitHub cheats in it's rendering: it replaces emojinames with pngs, and
+Note that GitHub cheats in its rendering: it replaces emoji names with pngs, and
 includes some emojis which are not supported by the unicode standard. We don't
 stand for this standardless stuff at the moment, because it would be too tedious
 to implement.
@@ -62,7 +62,9 @@ We provide a custom TLA+ syntax highlighting plugin for [highlight.js][] in `hig
 
 #### Building
 
-The plugin is checked in with the source code, and you generally shouldn't need to rebuild it unless you need to make a change or update the plugin.
+The plugin is checked in with the source code,
+and you generally shouldn't need to rebuild it
+unless you need to make a change or update the plugin.
 
 To build, check out the main highlight.js into a separate directory.
 Symlink the TLA+ language definition into the highlight.js `extra` directory:

docs/internal/dev/using-bloop.md

@@ -1,7 +1,7 @@
 # Developing with bloop
 
 [Bloop](https://scalacenter.github.io/bloop/) is a build server that can yield
-lightening fast incremental builds of Scala projects.
+lightning fast incremental builds of Scala projects.
 
 It is used by [Scala Metals](https://scalameta.org/metals/), but is also very
 useful as a standalone to save devs from the pain of `mvn`.

docs/internal/smt/Cardinality.md

@@ -203,7 +203,7 @@ By collecting the constraints in this section, `[DefCin]` and `[Repr]`, we have
 a complete set of constraints for computing `k_n = Cardinality(S)`. As one can
 see, the number of literals in this encoding is **linear**, that is, `O(n)`.
 
-**NOTE:** Although the number of constraints is linear, we have to analyze complexity
+**NOTE:** Although the number of constraints is linear, we have to analyze the complexity 
 of the underlying SMT problem, which may happen to be as hard as the SMT problem
 that is constructed in v0.6.0.
 

docs/internal/types-api.md

@@ -5,7 +5,7 @@ Type reconstruction API
 
 In this note, we focus on the client interface of a type inference engine for TLA+.
 In the following, we refer to this interface as ``TI``.
-By fixing this interface we give the users the freedom of choosing from several
+By fixing this interface, we give the users the freedom of choosing from several
 type inference engines.
 
 Given a TLA+ expression ``ex``, the ultimate goal of type inference is to assign a type
@@ -25,16 +25,16 @@ An implementation of ``TI`` _must_ support two main phases of operation:
    1. Resolving operator overloading, e.g., the expressions ``<<1, 2>>`` and ``f[e]``
     can be treated as expressions either over tuples, or sequences.
 
-   1. Finding signatures for operator definitions, e.g., ``F(x) == x + 1`` should have
+   2. Finding signatures for operator definitions, e.g., ``F(x) == x + 1`` should have
     the signature ``Int => Int``.
 
    If successful, the results of this analysis should be stored somewhere for the subsequent use
    in the _Type computation_ mode. Note that it is not necessary to store the types of all the intermediate
-   subexpressions -- that would be wasteful. This analysis should store only the results that cannot
+   subexpressions - that would be wasteful. This analysis should store only the results that cannot
    be deterministically computed in the next phase such as resolved operator signatures and types of the variables.
    ``TIE`` _may_ use expression identifiers to save the type information in some storage.
 
-1. **Type computation**. In this phase, the client queries ``TIE`` by giving a ``TLA+`` expression
+2. **Type computation**. In this phase, the client queries ``TIE`` by giving a ``TLA+`` expression
     and the types of its arguments. ``TIE`` computes and returns the resulting type of the expression.
     For instance, given the expression ``F(e)`` and the type ``Int`` of ``e``, ``TIE`` finds the signature
     ``F: 'a -> 'a`` in its internal storage and returns the type ``Int``. Given the expression ``{x, y}``
@@ -44,7 +44,7 @@ An implementation of ``TI`` _must_ support two main phases of operation:
     ``TIE`` _must_ return the resulting type. **Importantly**, ``TIE`` _must_ assume that it can be given expressions
     that have not been analyzed in the first stage. Such expressions may originate from the rewriting techniques
     used by the client. In this case, ``TIE`` _must_ try to compute the resulting type. Only if the resulting type
-    cannot be deterministically computed (e.g., there is not relevant type information in the storage),
+    cannot be deterministically computed (e.g., there is no relevant type information in the storage),
     should ``TIE`` fail.
 
 

docs/src/HOWTOs/howto-write-type-annotations.md

@@ -21,14 +21,13 @@
    were removed in version 0.23.1.
 
  - Version 0.15.0: This HOWTO discusses how to write type annotations for the type checker
-   [Snowcat][], which is used in Apalache since version 0.15.0 (introduced in
-   2021).
+   [Snowcat][], which is used in Apalache since version 0.15.0 (introduced in 2021).
 
 This HOWTO gives you concrete steps to extend TLA+ specifications with type
 annotations. You can find the detailed syntax of type annotations in
 [ADR002][]. The first rule of writing type annotations:
 
-*Do not to write any annotations at all, until the type checker [Snowcat][] is
+*Do not write any annotations at all, until the type checker [Snowcat][] is
 asking you to write a type annotation.*
 
 Of course, there must be an exception to this rule. You have to write type
@@ -128,10 +127,10 @@ Have a look at the type of `chan`:
 ```
 
 The type of `chan` is a record that has three fields: field `val` of type
-`DATUM`, field `rdy` of type `Int`, field `ack` of type `Int`. The record type syntax is similar to dictionary syntax from programming languages (e.g. Python). We made it different
-from TLA+'s syntax for records `[ val |-> v, rdy |-> r, ack |-> a ]`
-and record sets `[ val: V, rdy: R, ack: A ]`, to avoid confusion between
-types and values.
+`DATUM`, field `rdy` of type `Int`, field `ack` of type `Int`.
+The record type syntax is similar to dictionary syntax from programming languages (e.g. Python).
+We made it different from TLA+'s syntax for records `[ val |-> v, rdy |-> r, ack |-> a ]`
+and record sets `[ val: V, rdy: R, ack: A ]`, to avoid confusion between types and values.
 
 Run the type checker again. You should see the following message:
 
@@ -441,9 +440,9 @@ For more details on the design and usage, see [Type Aliases][] in ADR-002.
 
 ## Recipe 7: Multi-line annotations
 
-A type annotation may span over multiple lines. You may use both the `(* ...
-*)` syntax as well as the single-line syntax `\* ...`. All three examples below
-are accepted by the parser:
+A type annotation may span over multiple lines. You may use both the `(* ... *)`
+syntax as well as the single-line syntax `\* ...`.
+All three examples below are accepted by the parser:
 
 ```tla
 VARIABLES
@@ -467,8 +466,8 @@ similar to how multi-line strings are treated in modern programming languages.
 
 ## Recipe 8: Comments in annotations
 
-Sometimes, it helps to document the meaning of type components. Consider the following
-example from [Recipe 5](#funAsSeq):
+Sometimes, it helps to document the meaning of type components.
+Consider the following example from [Recipe 5](#funAsSeq):
 
 ```tla
 \* @type: (Seq(Int), Int, Int) => Bool;
@@ -571,7 +570,7 @@ a type annotation before the keyword `LOCAL`, not after it. For example:
 LOCAL LocalInc(x) == x + 1
 ```
 
-This may change later, when the tlaplus [Issue 578][] is resolved.
+This may change later when the tlaplus [Issue 578][] is resolved.
 
 
 [old type annotations]: ../apalache/types-and-annotations.md

docs/src/HOWTOs/uninterpretedTypes.md

@@ -1,23 +1,32 @@
 # How to use uninterpreted types
 
-This HOWTO explains what uninterpreted types are in the context of Apalache's type system, outlined in [ADR002][], and where/how to use them.
+This HOWTO explains what uninterpreted types are in the context of Apalache's type system,
+outlined in [ADR002][], and where/how to use them.
 
 ## What are uninterpreted types?
-It is often the case, when writing specifications, that inputs (`CONSTANTS`) describe a collection of values, where the only relevant property is that all of the values are considered unique. For instance, [TwoPhase.tla][] defines 
+It is often the case, when writing specifications, that inputs (`CONSTANTS`) describe a collection of values,
+where the only relevant property is that all the values are considered unique.
+For instance, [TwoPhase.tla][] defines 
 ```tla
 CONSTANT RM \* The set of resource managers
 ```
-however, for the purposes of specification analysis, it does not matter if we instantiate 
-`RM = 1..3` or `RM = {"a","b","c"}`, because the only operators applied to elements of `RM` are polymorphic in the type of the elements of `RM`.
+however, for the purposes of specification analysis,
+it does not matter if we instantiate `RM = 1..3` or `RM = {"a","b","c"}`,
+because the only operators applied to elements of `RM` are polymorphic in the type of the elements of `RM`.
 
 For this reason, Apalache supports a special kind of type annotation: uninterpreted types. 
-The type checker [Snowcat][] makes sure that a value belonging to an uninterpreted type is only ever passed to polymorphic operators, and, importantly, that it is never compared to a value of any other type. 
+The type checker [Snowcat][] makes sure that a value belonging to an uninterpreted type
+is only ever passed to polymorphic operators, and, importantly, that it is never compared to a value of any other type. 
 
 ## When to use uninterpreted types?
 
-For efficiency reasons, you should use uninterpreted types whenever a `CONSTANT` or value represents (an element of) a collection of unique identifiers, the precise value of which does not influence the properties of the specification.
+For efficiency reasons, you should use uninterpreted types whenever a `CONSTANT` or value
+represents (an element of) a collection of unique identifiers,
+the precise value of which does not influence the properties of the specification.
 
-On the other hand, if, for example, the order of values matters, identifiers should likely be `1..N` and hold type `Int` instead of an uninterpreted type, since `Int` values can be passed to the non-polymorphic `<,>,>=,<=` operators.
+On the other hand, if, for example, the order of values matters,
+identifiers should likely be `1..N` and hold type `Int` instead of an uninterpreted type,
+since `Int` values can be passed to the non-polymorphic `<,>,>=,<=` operators.
 
 ## How to annotate uninterpreted types
 Following [ADR002][], an annotation with an uninterpreted type looks exactly like an annotation with a type alias:
@@ -36,13 +45,17 @@ where:
   - `TYPENAME` is the uninterpreted type to which this value belongs, matching the pattern `[A-Z_][A-Z0-9_]*`, and
   - `identifier` is a unique identifier within the uninterpreted type, matching the pattern `[a-zA-Z0-9_]+`.
 
-Example: `"1_OF_UT"` is a value belonging to the uninterpreted type `UT`, as is `"2_OF_UT"`. These two values are distinct by definition. On the contrary,
-`"1_OF_ut"` does _not_ meet the criteria for a value belonging to an uninterpreted type ( lowercase `ut` is not a valid identifier for an uninterpreted type), so it is treated as a string value.
+Example: `"1_OF_UT"` is a value belonging to the uninterpreted type `UT`, as is `"2_OF_UT"`.
+These two values are distinct by definition.
+On the contrary, `"1_OF_ut"` does _not_ meet the criteria for a value belonging to an uninterpreted type
+(lowercase `ut` is not a valid identifier for an uninterpreted type), so it is treated as a string value.
 
-**Note**: Values matching the pattern `"FRESH[0-9]+_OF_TYPENAME"` are reserved for internal use, to allow Apalache to construct fresh values.
+**Note**: Values matching the pattern `"FRESH[0-9]+_OF_TYPENAME"` are reserved for internal use,
+to allow Apalache to construct fresh values.
 
 ## Uninterpreted types, `Str`, and comparisons
-Importantly, while both strings and values belonging to uninterpreted types are introduced using the `"..."` notation, they are treated as having distinct, incomparable types.
+Importantly, while both strings and values belonging to uninterpreted types are introduced using the `"..."` notation,
+they are treated as having distinct, incomparable types.
 Examples:
   - The following expression is type-incorrect:
     ```tla 

docs/src/apalache/antipatterns.md

@@ -1,8 +1,13 @@
 # Antipatterns
 
-This page collects known antipaterns (APs) when writing TLA+ for Apalache. In this context, APs are syntactic forms or specification approaches that, for one reason or another, have particularly slow/complex encodings for the target model checker. For a pattern to be an AP, there must exist a known, equivalent, efficient pattern. 
+This page collects known antipaterns (APs) when writing TLA+ for Apalache.
+In this context, APs are syntactic forms or specification approaches that,
+for one reason or another, have particularly slow/complex encodings for the target model checker.
+For a pattern to be an AP, there must exist a known, equivalent, efficient pattern. 
 
-Often, APs arise from a user's past experiences with writing TLA+ for TLC, or from a direct translation of imperative OOP code into TLA+, as those follow a different paradigm, and therefore entail different cost evaluation of which expressions are slow/complex and which are not.
+Often, APs arise from a user's past experiences with writing TLA+ for TLC,
+or from a direct translation of imperative OOP code into TLA+, as those follow a different paradigm,
+and therefore entail different cost evaluation of which expressions are slow/complex and which are not.
 
 ## `CHOOSE`-based recursion
 
@@ -29,9 +34,11 @@ min(S) ==
     IN IF e < minOther THEN e ELSE minOther 
 ```
 
-Apalache dislikes the use of the above, for several reasons. Firstly, since the operator is `RECURSIVE`, Apalache does not support it after version 0.23.1. In earlier versions Apalache requires a predefined upper bound on unrolling, which means that the user must know, ahead of time, what the largest `|S|` is, for any set `S`, to which this operator is ever applied. 
+Apalache dislikes the use of the above, for several reasons. Firstly, since the operator is `RECURSIVE`,
+Apalache does not support it after version 0.23.1. In earlier versions Apalache requires a predefined upper bound on unrolling,
+which means that the user must know, ahead of time, what the largest `|S|` is, for any set `S`, to which this operator is ever applied. 
 In addition, computing `F` for a set `S` of size `n = |S|` requires `n` encodings of a `CHOOSE` operation, which can be considerably expensive in Apalache.
-Lastly, Apalache also needs to encode all of the the `n` intermediate sets, `S \ {e1}`, `(S \ {e1}) \ {e2}`, `((S \ {e1}) \ {e2}) \ {e3}`, and so on.
+Lastly, Apalache also needs to encode all the the `n` intermediate sets, `S \ {e1}`, `(S \ {e1}) \ {e2}`, `((S \ {e1}) \ {e2}) \ {e3}`, and so on.
 
 The AP above can be replaced by a very simple pattern:
 ```tla
@@ -41,7 +48,10 @@ F(S) == ApaFoldSet( G, v, S )
 `ApaFoldSet` (and `ApaFoldSeqLeft`) were introduced precisely for these scenarios, and should be used over `RECURSIVE + CHOOSE` in most cases.
 
 ## Incremental computation
-Often, users introduce an expression `Y`, which is derived from another expression `X` (`Y == F(X)`, for some `F`). Instead of defining `Y` directly, in terms of the properties it possesses,  it is possible to define all the intermediate steps of transforming `X` into `Y`: "`X` is slightly changed into `X1` (e.g. by adding one element to a set, or via `EXCEPT`), which is changed into `X2`, etc. until `Xn = Y`". Doing this in Apalache is almost always a bad idea, if a direct characterization of `Y` exists.
+Often, users introduce an expression `Y`, which is derived from another expression `X` (`Y == F(X)`, for some `F`).
+Instead of defining `Y` directly, in terms of the properties it possesses, it is possible to define all the intermediate
+steps of transforming `X` into `Y`: "`X` is slightly changed into `X1` (e.g. by adding one element to a set, or via `EXCEPT`),
+which is changed into `X2`, etc. until `Xn = Y`". Doing this in Apalache is almost always a bad idea, if a direct characterization of `Y` exists.
 
 Concretely, the following constructs are APs:
 1. Incremental `EXCEPT`
@@ -73,7 +83,10 @@ Y ==
 
 TLC likes these sorts of operations, because it manipulates programming-language objects in its own implementation.
 This makes it easy to construct temporary mutable objects, manipulate them (e.g. via for-loops) and garbage-collect them after they stop being useful.
-For constraint-based approaches, like Apalache, the story is different. Not only are these intermediate steps not directly useful (since Apalache is not modeling TLA+ expressions as objects in Sacala), they actually hurt performance, since they can generate a significant amount of constraints, which are all about describing data structures (e.g. two functions being almost equal, except at one point).
+For constraint-based approaches, like Apalache, the story is different.
+Not only are these intermediate steps not directly useful (since Apalache is not modeling TLA+ expressions as objects in Scala),
+they actually hurt performance, since they can generate a significant amount of constraints,
+which are all about describing data structures (e.g. two functions being almost equal, except at one point).
 Essentially, Apalache is spending its resources not on state-space exploration, but on in-state value computation, which is not its strong suit.
 Below we show how to rewrite these APs.
 
@@ -112,4 +125,3 @@ with
 ```tla
 f == [ k \in {k1,...,kn} |-> A(k) ]
 ```
-

docs/src/apalache/assignments-in-depth.md

@@ -346,7 +346,7 @@ Lastly, while `E` looks almost identical to `A`, the key difference is that
 expressions under universal quantifiers may not contain assignments. Therefore,
 `y' = s` is *not* an assignment to `y` and thus violates assignment-before-use.
 
-<a name='manual' /> 
+<a name='manual'></a>
 ## Manual Assignments
 
 Users may choose, but aren't required, to use manual assignments `x' := e` in

docs/src/apalache/config.md

@@ -51,7 +51,7 @@ common  {
 }
 ```
 
-A `~` found at the beginning of a file path will expanded into the value set for
+A `~` found at the beginning of a file path will be expanded into the value set for
 the user's home directory.
 
 Details on the effect of these parameters can be found in [Running the