deploy: f4176fd

docs/HOWTOs/howto-write-type-annotations.html

@@ -196,14 +196,13 @@ <h1><a class="header" href="#how-to-write-type-annotations" id="how-to-write-typ
 </li>
 <li>
 <p>Version 0.15.0: This HOWTO discusses how to write type annotations for the type checker
-<a href="../apalache/typechecker-snowcat.html">Snowcat</a>, which is used in Apalache since version 0.15.0 (introduced in
-2021).</p>
+<a href="../apalache/typechecker-snowcat.html">Snowcat</a>, which is used in Apalache since version 0.15.0 (introduced in 2021).</p>
 </li>
 </ul>
 <p>This HOWTO gives you concrete steps to extend TLA+ specifications with type
 annotations. You can find the detailed syntax of type annotations in
 <a href="../adr/002adr-types.html">ADR002</a>. The first rule of writing type annotations:</p>
-<p><em>Do not to write any annotations at all, until the type checker <a href="../apalache/typechecker-snowcat.html">Snowcat</a> is
+<p><em>Do not write any annotations at all, until the type checker <a href="../apalache/typechecker-snowcat.html">Snowcat</a> is
 asking you to write a type annotation.</em></p>
 <p>Of course, there must be an exception to this rule. You have to write type
 annotations for CONSTANTS and VARIABLES. This is because Snowcat infers types
@@ -311,10 +310,10 @@ <h2><a class="header" href="#recipe-2-annotating-constants" id="recipe-2-annotat
 <pre><code>\* @type: { val: DATUM, rdy: Int, ack: Int };
 </code></pre>
 <p>The type of <code>chan</code> is a record that has three fields: field <code>val</code> of type
-<code>DATUM</code>, field <code>rdy</code> of type <code>Int</code>, field <code>ack</code> of type <code>Int</code>. 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 <code>[ val |-&gt; v, rdy |-&gt; r, ack |-&gt; a ]</code>
-and record sets <code>[ val: V, rdy: R, ack: A ]</code>, to avoid confusion between
-types and values.</p>
+<code>DATUM</code>, field <code>rdy</code> of type <code>Int</code>, field <code>ack</code> of type <code>Int</code>.
+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 <code>[ val |-&gt; v, rdy |-&gt; r, ack |-&gt; a ]</code>
+and record sets <code>[ val: V, rdy: R, ack: A ]</code>, to avoid confusion between types and values.</p>
 <p>Run the type checker again. You should see the following message:</p>
 <pre><code>$ apalache-mc typecheck ChannelTyped.tla
 ...
@@ -571,8 +570,9 @@ <h2><a class="header" href="#recipe-6-type-aliases" id="recipe-6-type-aliases">R
 alias, instead of changing the record type everywhere.</p>
 <p>For more details on the design and usage, see <a href="../adr/002adr-types.html#defTypeAlias">Type Aliases</a> in ADR-002.</p>
 <h2><a class="header" href="#recipe-7-multi-line-annotations" id="recipe-7-multi-line-annotations">Recipe 7: Multi-line annotations</a></h2>
-<p>A type annotation may span over multiple lines. You may use both the <code>(* ... *)</code> syntax as well as the single-line syntax <code>\* ...</code>. All three examples below
-are accepted by the parser:</p>
+<p>A type annotation may span over multiple lines. You may use both the <code>(* ... *)</code>
+syntax as well as the single-line syntax <code>\* ...</code>.
+All three examples below are accepted by the parser:</p>
 <pre><code class="language-tla">VARIABLES
    (*
     @type: Int
@@ -591,8 +591,8 @@ <h2><a class="header" href="#recipe-7-multi-line-annotations" id="recipe-7-multi
 <p>Note that the parser removes the leading strings <code>&quot;    \*&quot;</code> from the annotations,
 similar to how multi-line strings are treated in modern programming languages.</p>
 <h2><a class="header" href="#recipe-8-comments-in-annotations" id="recipe-8-comments-in-annotations">Recipe 8: Comments in annotations</a></h2>
-<p>Sometimes, it helps to document the meaning of type components. Consider the following
-example from <a href="#funAsSeq">Recipe 5</a>:</p>
+<p>Sometimes, it helps to document the meaning of type components.
+Consider the following example from <a href="#funAsSeq">Recipe 5</a>:</p>
 <pre><code class="language-tla">\* @type: (Seq(Int), Int, Int) =&gt; Bool;
 Attacks(queens,i,j)
 </code></pre>
@@ -679,7 +679,7 @@ <h3><a class="header" href="#annotations-of-local-operators" id="annotations-of-
 <pre><code class="language-tla">\* @type: Int =&gt; Int;
 LOCAL LocalInc(x) == x + 1
 </code></pre>
-<p>This may change later, when the tlaplus <a href="https://github.com/tlaplus/tlaplus/issues/578">Issue 578</a> is resolved.</p>
+<p>This may change later when the tlaplus <a href="https://github.com/tlaplus/tlaplus/issues/578">Issue 578</a> is resolved.</p>
 
                     </main>
 

docs/HOWTOs/uninterpretedTypes.html

@@ -171,18 +171,27 @@ <h1 class="menu-title">Apalache Documentation</h1>
                 <div id="content" class="content">
                     <main>
                         <h1><a class="header" href="#how-to-use-uninterpreted-types" id="how-to-use-uninterpreted-types">How to use uninterpreted types</a></h1>
-<p>This HOWTO explains what uninterpreted types are in the context of Apalache's type system, outlined in <a href="../adr/002adr-types.html">ADR002</a>, and where/how to use them.</p>
+<p>This HOWTO explains what uninterpreted types are in the context of Apalache's type system,
+outlined in <a href="../adr/002adr-types.html">ADR002</a>, and where/how to use them.</p>
 <h2><a class="header" href="#what-are-uninterpreted-types" id="what-are-uninterpreted-types">What are uninterpreted types?</a></h2>
-<p>It is often the case, when writing specifications, that inputs (<code>CONSTANTS</code>) describe a collection of values, where the only relevant property is that all of the values are considered unique. For instance, <a href="https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla">TwoPhase.tla</a> defines </p>
+<p>It is often the case, when writing specifications, that inputs (<code>CONSTANTS</code>) describe a collection of values,
+where the only relevant property is that all the values are considered unique.
+For instance, <a href="https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla">TwoPhase.tla</a> defines </p>
 <pre><code class="language-tla">CONSTANT RM \* The set of resource managers
 </code></pre>
-<p>however, for the purposes of specification analysis, it does not matter if we instantiate 
-<code>RM = 1..3</code> or <code>RM = {&quot;a&quot;,&quot;b&quot;,&quot;c&quot;}</code>, because the only operators applied to elements of <code>RM</code> are polymorphic in the type of the elements of <code>RM</code>.</p>
+<p>however, for the purposes of specification analysis,
+it does not matter if we instantiate <code>RM = 1..3</code> or <code>RM = {&quot;a&quot;,&quot;b&quot;,&quot;c&quot;}</code>,
+because the only operators applied to elements of <code>RM</code> are polymorphic in the type of the elements of <code>RM</code>.</p>
 <p>For this reason, Apalache supports a special kind of type annotation: uninterpreted types. 
-The type checker <a href="../apalache/typechecker-snowcat.html">Snowcat</a> 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. </p>
+The type checker <a href="../apalache/typechecker-snowcat.html">Snowcat</a> 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. </p>
 <h2><a class="header" href="#when-to-use-uninterpreted-types" id="when-to-use-uninterpreted-types">When to use uninterpreted types?</a></h2>
-<p>For efficiency reasons, you should use uninterpreted types whenever a <code>CONSTANT</code> or value represents (an element of) a collection of unique identifiers, the precise value of which does not influence the properties of the specification.</p>
-<p>On the other hand, if, for example, the order of values matters, identifiers should likely be <code>1..N</code> and hold type <code>Int</code> instead of an uninterpreted type, since <code>Int</code> values can be passed to the non-polymorphic <code>&lt;,&gt;,&gt;=,&lt;=</code> operators.</p>
+<p>For efficiency reasons, you should use uninterpreted types whenever a <code>CONSTANT</code> or value
+represents (an element of) a collection of unique identifiers,
+the precise value of which does not influence the properties of the specification.</p>
+<p>On the other hand, if, for example, the order of values matters,
+identifiers should likely be <code>1..N</code> and hold type <code>Int</code> instead of an uninterpreted type,
+since <code>Int</code> values can be passed to the non-polymorphic <code>&lt;,&gt;,&gt;=,&lt;=</code> operators.</p>
 <h2><a class="header" href="#how-to-annotate-uninterpreted-types" id="how-to-annotate-uninterpreted-types">How to annotate uninterpreted types</a></h2>
 <p>Following <a href="../adr/002adr-types.html">ADR002</a>, an annotation with an uninterpreted type looks exactly like an annotation with a type alias:</p>
 <pre><code class="language-tla">\* @type: UTNAME;
@@ -197,11 +206,15 @@ <h2><a class="header" href="#how-to-introduce-values-belonging-to-an-uninterpret
 <li><code>TYPENAME</code> is the uninterpreted type to which this value belongs, matching the pattern <code>[A-Z_][A-Z0-9_]*</code>, and</li>
 <li><code>identifier</code> is a unique identifier within the uninterpreted type, matching the pattern <code>[a-zA-Z0-9_]+</code>.</li>
 </ul>
-<p>Example: <code>&quot;1_OF_UT&quot;</code> is a value belonging to the uninterpreted type <code>UT</code>, as is <code>&quot;2_OF_UT&quot;</code>. These two values are distinct by definition. On the contrary,
-<code>&quot;1_OF_ut&quot;</code> does <em>not</em> meet the criteria for a value belonging to an uninterpreted type ( lowercase <code>ut</code> is not a valid identifier for an uninterpreted type), so it is treated as a string value.</p>
-<p><strong>Note</strong>: Values matching the pattern <code>&quot;FRESH[0-9]+_OF_TYPENAME&quot;</code> are reserved for internal use, to allow Apalache to construct fresh values.</p>
+<p>Example: <code>&quot;1_OF_UT&quot;</code> is a value belonging to the uninterpreted type <code>UT</code>, as is <code>&quot;2_OF_UT&quot;</code>.
+These two values are distinct by definition.
+On the contrary, <code>&quot;1_OF_ut&quot;</code> does <em>not</em> meet the criteria for a value belonging to an uninterpreted type
+(lowercase <code>ut</code> is not a valid identifier for an uninterpreted type), so it is treated as a string value.</p>
+<p><strong>Note</strong>: Values matching the pattern <code>&quot;FRESH[0-9]+_OF_TYPENAME&quot;</code> are reserved for internal use,
+to allow Apalache to construct fresh values.</p>
 <h2><a class="header" href="#uninterpreted-types-str-and-comparisons" id="uninterpreted-types-str-and-comparisons">Uninterpreted types, <code>Str</code>, and comparisons</a></h2>
-<p>Importantly, while both strings and values belonging to uninterpreted types are introduced using the <code>&quot;...&quot;</code> notation, they are treated as having distinct, incomparable types.
+<p>Importantly, while both strings and values belonging to uninterpreted types are introduced using the <code>&quot;...&quot;</code> notation,
+they are treated as having distinct, incomparable types.
 Examples:</p>
 <ul>
 <li>The following expression is type-incorrect:

docs/apalache/antipatterns.html

@@ -171,8 +171,13 @@ <h1 class="menu-title">Apalache Documentation</h1>
                 <div id="content" class="content">
                     <main>
                         <h1><a class="header" href="#antipatterns" id="antipatterns">Antipatterns</a></h1>
-<p>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. </p>
-<p>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.</p>
+<p>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. </p>
+<p>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.</p>
 <h2><a class="header" href="#choose-based-recursion" id="choose-based-recursion"><code>CHOOSE</code>-based recursion</a></h2>
 <p>Often, operators that represent operations over sets have the following shape:</p>
 <pre><code class="language-tla">RECURSIVE F(_)
@@ -193,15 +198,20 @@ <h2><a class="header" href="#choose-based-recursion" id="choose-based-recursion"
     IN LET minOther == min( S \ {e} )
     IN IF e &lt; minOther THEN e ELSE minOther 
 </code></pre>
-<p>Apalache dislikes the use of the above, for several reasons. Firstly, since the operator is <code>RECURSIVE</code>, 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 <code>|S|</code> is, for any set <code>S</code>, to which this operator is ever applied. 
+<p>Apalache dislikes the use of the above, for several reasons. Firstly, since the operator is <code>RECURSIVE</code>,
+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 <code>|S|</code> is, for any set <code>S</code>, to which this operator is ever applied. 
 In addition, computing <code>F</code> for a set <code>S</code> of size <code>n = |S|</code> requires <code>n</code> encodings of a <code>CHOOSE</code> operation, which can be considerably expensive in Apalache.
-Lastly, Apalache also needs to encode all of the the <code>n</code> intermediate sets, <code>S \ {e1}</code>, <code>(S \ {e1}) \ {e2}</code>, <code>((S \ {e1}) \ {e2}) \ {e3}</code>, and so on.</p>
+Lastly, Apalache also needs to encode all the the <code>n</code> intermediate sets, <code>S \ {e1}</code>, <code>(S \ {e1}) \ {e2}</code>, <code>((S \ {e1}) \ {e2}) \ {e3}</code>, and so on.</p>
 <p>The AP above can be replaced by a very simple pattern:</p>
 <pre><code class="language-tla">F(S) == ApaFoldSet( G, v, S )
 </code></pre>
 <p><code>ApaFoldSet</code> (and <code>ApaFoldSeqLeft</code>) were introduced precisely for these scenarios, and should be used over <code>RECURSIVE + CHOOSE</code> in most cases.</p>
 <h2><a class="header" href="#incremental-computation" id="incremental-computation">Incremental computation</a></h2>
-<p>Often, users introduce an expression <code>Y</code>, which is derived from another expression <code>X</code> (<code>Y == F(X)</code>, for some <code>F</code>). Instead of defining <code>Y</code> directly, in terms of the properties it possesses,  it is possible to define all the intermediate steps of transforming <code>X</code> into <code>Y</code>: &quot;<code>X</code> is slightly changed into <code>X1</code> (e.g. by adding one element to a set, or via <code>EXCEPT</code>), which is changed into <code>X2</code>, etc. until <code>Xn = Y</code>&quot;. Doing this in Apalache is almost always a bad idea, if a direct characterization of <code>Y</code> exists.</p>
+<p>Often, users introduce an expression <code>Y</code>, which is derived from another expression <code>X</code> (<code>Y == F(X)</code>, for some <code>F</code>).
+Instead of defining <code>Y</code> directly, in terms of the properties it possesses, it is possible to define all the intermediate
+steps of transforming <code>X</code> into <code>Y</code>: &quot;<code>X</code> is slightly changed into <code>X1</code> (e.g. by adding one element to a set, or via <code>EXCEPT</code>),
+which is changed into <code>X2</code>, etc. until <code>Xn = Y</code>&quot;. Doing this in Apalache is almost always a bad idea, if a direct characterization of <code>Y</code> exists.</p>
 <p>Concretely, the following constructs are APs:</p>
 <ol>
 <li>Incremental <code>EXCEPT</code></li>
@@ -230,7 +240,10 @@ <h2><a class="header" href="#incremental-computation" id="incremental-computatio
 </code></pre>
 <p>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.</p>
 <ol>

docs/apalache/assignments-in-depth.html

@@ -435,8 +435,8 @@ <h3><a class="header" href="#assignment-free-expressions" id="assignment-free-ex
 <p>Lastly, while <code>E</code> looks almost identical to <code>A</code>, the key difference is that
 expressions under universal quantifiers may not contain assignments. Therefore,
 <code>y' = s</code> is <em>not</em> an assignment to <code>y</code> and thus violates assignment-before-use.</p>
-<a name='manual' /> 
-## Manual Assignments
+<p><a name='manual'></a></p>
+<h2><a class="header" href="#manual-assignments" id="manual-assignments">Manual Assignments</a></h2>
 <p>Users may choose, but aren't required, to use manual assignments <code>x' := e</code> in
 place of <code>x' = e</code>.  While the use of this operator does not change Apalache's
 internal search for assignments (in particular, using manual assignment

docs/apalache/config.html

@@ -211,7 +211,7 @@ <h3><a class="header" href="#file-format-and-supported-parameters" id="file-form
     # run-dir = ~/my-run-dir
 }
 </code></pre>
-<p>A <code>~</code> found at the beginning of a file path will expanded into the value set for
+<p>A <code>~</code> found at the beginning of a file path will be expanded into the value set for
 the user's home directory.</p>
 <p>Details on the effect of these parameters can be found in <a href="./running.html">Running the
 Tool</a>.</p>