Merge branch 'main' into change-tuple-structure

CHANGELOG.md

@@ -14,6 +14,44 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Fixed
 ### Security
 
+## v0.22.3 -- 2024-10-28
+
+### Added
+
+- Added a new operator called `getOnlyElement()` to extract elements out of singleton sets (#1525)
+
+### Changed
+
+- Updated grammar rule to allow an optional trailing comma in parameter lists (#1510):
+  - Operator calls
+  - Constant initialization
+  - Operator definitions
+
+### Deprecated
+### Removed
+### Fixed
+
+- The seed was not being properly printed when the simulator found some runtime errors (#1524).
+- Fixed a problem where using `--mbt` resulted in missing data on `nondet_picks`
+  due to internal caching (#1531)
+- Hashbang lines are now properly highlighted as comments in vscode and in highlight.js.
+
+### Security
+
+## v0.22.2 -- 2024-10-08
+
+### Added
+
+- `quint verify` has the option `--apalache-version` to pull a custom version (#1521)
+- Grammar updated with support for an optional leading hashbang (`#!`) line (#1522)
+
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+### Security
+
 ## v0.22.1 -- 2024-09-25
 
 ### Added
@@ -25,6 +63,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Some error scenarios when importing files on Windows were fixed (#1498)
 - `quint verify` on Windows should now properly start an Apalache server on the
   background (#1499)
+- `quint verify` on Linux properly terminates the spawned instance (#1520)
 
 ### Security
 

docs/components/faq/FAQBox.tsx

@@ -0,0 +1,49 @@
+import { useState, useEffect } from "react";
+
+export function FAQBox({ title, children }) {
+  const id = title.toLowerCase().replace(/[/?]/g, "").replace(/\s+/g, "-");
+  useEffect(() => {
+    const handleHashChange = () => {
+      const element = document.getElementById(id);
+      if (element && window.location.hash === `#${id}` && "open" in element) {
+        element.open = true;
+        element.scrollIntoView();
+      }
+    };
+
+    const handleAnchorClick = (event) => {
+      const anchor = event.target.closest("a");
+      if (anchor && anchor.hash === `#${id}`) {
+        const element = document.getElementById(id);
+        if (element && "open" in element) {
+          element.open = true;
+          element.scrollIntoView();
+        }
+      }
+    };
+
+    window.addEventListener("hashchange", handleHashChange);
+    document.addEventListener("click", handleAnchorClick);
+    handleHashChange();
+
+    return () => {
+      window.removeEventListener("hashchange", handleHashChange);
+      document.removeEventListener("click", handleAnchorClick);
+    };
+  }, [id]);
+
+  return (
+    <details
+      className="last-of-type:mb-0 rounded-lg bg-neutral-50 dark:bg-neutral-800 p-2 mt-4"
+      id={id}
+      onClick={() => {
+        window.history.pushState({}, "", `#${id}`);
+      }}
+    >
+      <summary>
+        <strong className="text-lg">{title}</strong>
+      </summary>
+      <div className="nx-p-2">{children}</div>
+    </details>
+  );
+}

docs/pages/docs/builtin.md

@@ -306,6 +306,19 @@ assert(Set(1, 2).allListsUpTo(1) == Set([], [1], [2]))
 assert(Set(1).allListsUpTo(2) == Set([], [1], [1, 1]))
 ```
 
+## getOnlyElement
+
+Signature: `pure def getOnlyElement: (Set[a]) => a`
+
+`s.getOnlyElement()` is, deterministically, the only element of `s`.
+If the size of `s` is not 1, this operator has undefined behavior.
+
+### Examples
+
+```quint
+assert(Set(5).getOnlyElement() == 5)
+```
+
 ## chooseSome
 
 Signature: `pure def chooseSome: (Set[a]) => a`

docs/pages/docs/faq.mdx

@@ -1,20 +1,10 @@
+import { FAQBox } from '../../components/faq/FAQBox'
+
 # Frequently Asked Questions
 Here you can find answers to the questions that are often asked by people who
 would like to start with Quint.
 
 <br />
-export function FAQBox({ title, children }) {
-  return (
-    <details
-      className="last-of-type:mb-0 rounded-lg bg-neutral-50 dark:bg-neutral-800 p-2 mt-4"
-    >
-      <summary>
-        <strong className="text-lg">{title}</strong>
-      </summary>
-      <div className="nx-p-2">{children}</div>
-    </details>
-  )
-}
 
 <FAQBox title="How does Quint compare to fuzzing?">
 Main similarities:
@@ -52,6 +42,195 @@ defined and incompatible interfaces - which are the biggest problems in common
 specifications.
 </FAQBox>
 
+<FAQBox title="How does Quint compare to TLA+?">
+
+Quint is based on TLA+ and uses the same underlying logic (Temporal Logic of
+Actions), so it is very similar to TLA+ in terms of where it is useful. The main
+differences between Quint and TLA+ are:
+1. Quint has programming-style syntax, while TLA+ uses math/latex symbols.
+2. Quint has more static analysis, such as type checking and different modes
+   (`pure def`, `action`, etc), while TLA+ has no native support for types nor
+   explicit distinction between the modes (or levels, as they are called in
+   TLA+'s documentation).
+3. Quint tooling is more similar to what we have for programming languages:
+   near-instant feedback as you type the code, CLI-first executable, an easy way
+   to obtain one execution of your spec in the terminal, a REPL, located error
+   messages, etc. These are all not currently available in TLA+, or available
+   with significant constraints.
+4. Quint won't let you write many things that are allowed in TLA+. TLA+ has a
+   proof system (TLAPS), while Quint doesn't. Therefore, it is possible to write
+   more advanced formulas in TLA+ than in Quint, even ones that are not
+   supported by the existing model checkers, and then prove them using the proof
+   system. Quint restricts you to a fragment of TLA with the intention of
+   preventing unintentional usage of operators that lead to complicated
+   behaviors that are hard to debug and understand. Our understanding is that
+   anything outside of Quint's fragment is only written by people with a strong
+   mathematical mindset, and those people will probably appreciate TLA+'s
+   mathematical syntax much better.
+5. Quint has the concept of a `run` to define executions to be used as tests.
+   There is no corresponding feature in TLA+.
+6. TLA+ has model values and symmetry sets, which are not available in Quint at
+   this time.
+
+On a less concrete note, TLA+ supporters will often say that the mathematical
+syntax helps to put people in the correct mindset of formal specification,
+while Quint as a project hopes to teach people this mindset without a big syntax
+and tool disruption.
+</FAQBox>
+
+<FAQBox title="Is Quint the same thing as PlusCal?">
+No. Although both Quint and PlusCal have the goal of making TLA+ more
+approachable to engineers, the strategies are very different. PlusCal uses the
+same tooling and similar syntax to TLA+, but introduces imperative constructs
+(while TLA+ is fully declarative). Quint, on the other hand, introduces new
+tooling and syntax, but keeps the declarative aspect.
+
+It would be possible to add the imperative constructs from PlusCal to Quint. We
+currently don't have a lot of clarity on how useful that would be.
+
+We experienced situations where the expressiveness constraints imposed by PlusCal were a
+problem for some of our systems, while Quint has always been enough.
+</FAQBox>
+
+
+<FAQBox title="How does Quint compare to Alloy?">
+
+Alloy is very focused on sets, and is good for specifying requirements and data
+structures, while Quint is natively time oriented, fitting really well with
+concurrent and distributed systems. As everything in Alloy is a set/relation, it
+requires a quite abstract and specific way of modeling.
+
+While Alloy 6 added temporal operators, for the longest time,
+handling the passage of time required complex workarounds, and
+therefore having the language be used mostly for other things.
+
+Alloy verification can be faster than Quint for specifications without time, as
+it can use SAT solving instead of SMT solving, and the tooling looks very
+different, with Alloy Analyzer being very visual.
+
+</FAQBox>
+
+<FAQBox title="How does Quint compare to Coq/Isabelle/Lean?">
+Coq, Isabelle and Lean are proof assistants. They will assist you to write a
+proof, but you still have to do most of the work. Quint uses model checking,
+where you only need to define the model and the properties, and the verification
+process is fully automated. Learning and mastering how to use a proof assistant
+is much harder (usually taking years) than learning and mastering Quint.
+
+Proof assistants require you to write deductive proofs, while model checkers (as
+in Quint), use an inductive approach, exploring all reachable states in a model.
+Proof assistants are mostly used for research, and model checking techniques are
+more present in the industry. Some instances of proof assistants in the industry
+do exist, as some properties of [DemiBFT (formerly
+LibraBFT)](https://github.com/novifinancial/LibraChain/) and [ZK circuit
+verifiers](https://veridise.com/wp-content/uploads/2023/09/VAR-RLN.pdf) being
+proven with Coq. However, it is a lot of work formalize and prove real systems
+and protocols, and proof assistants are used in much smaller scopes than what
+Quint is set up for.
+
+Proving something using one of these tools provides a much stronger guarantee
+than verifying something with a model checker. Proof assistants are software and
+thus can have bugs too, but they are generally more trustworthy than model
+checkers because they usually rely on a small kernel implementing the core
+logical rules. All proofs reduce to the rules in the kernel. The kernel is very
+small, probably a few hundred lines of code, so it's easier to check and trust
+that it faithfully implement the rules. Model checkers are much larger
+implementations and, therefore, more prone to bugs.
+
+While proof assistants enable very general proofs (such as `length(m) +
+length(n) = length(m + n)`), model checkers will always operate over some
+constraint state space (i.e. integers between 0 and 2^256).
+
+Another difference is that these tools are able to generate code from the
+formalization, meaning the code will be correct by construction. For example,
+you can generate Haskell code from Coq. This is very useful if you want to
+extract some sequential library, but code for distributed systems definitions
+might not be so applicable to real world usage.
+
+</FAQBox>
+
+<FAQBox title="How does Quint compare to Agda/Idris?">
+
+Agda and Idris are programming languages, while Quint is a specification
+language. Even so, Agda and Idris are formal methods tools, because you can
+write formal specification through dependent types, typing your program in a way
+that guarantees it has a certain behavior.
+
+They also work as proof systems (see ["How does Quint compare to
+Coq/Isabelle/Lean?"](#how-does-quint-compare-to-coqisabellelean)) and,
+similarly, they require a lot of expertise and time to prove things. Proving
+through dependent types shifts some of this burden to the type system, but still
+demand an advanced understanding. Model checking (as in Quint) will usually
+provide weaker guarantees in comparison, but the proofs are fully automated.
+
+Another difference is that programs in Agda and Idris need to be total - that
+is, they need to terminate, and the writer may need to convince the type system
+that in fact it does terminate every time.
+
+</FAQBox>
+
+<FAQBox title="How does Quint compare to Abstract State Machines?">
+
+Abstract State Machines (ASMs) are a precise way to write pseudocode to define
+the requirements of a system, and they are mostly used to reason about and
+analyze designs, while Quint is more focused on executing and verifying
+specifications.
+
+This [report](https://arxiv.org/abs/2301.10875) explores the differences and
+similarities between Quint, TLA+ and ASM in more detail.
+
+</FAQBox>
+
+<FAQBox title="How does Quint compare to tools for specific programming languages?">
+
+There is a big advantage and a big disadvantage for using some
+formal verification tool designed for your programming language of choice instead of using Quint.
+- Advantage: you don't have to write a Quint specification, you can use your own code
+- Disadvantage: the verification capabilities will be extremely limited, because
+  reasoning about generic programming language constructs and concrete program
+  states is incredibly complex.
+
+More generally, the state space of programs are often really large and
+unfeasible for any tool to handle. The solution is to abstract things and work
+on a higher level. Doing so in the same programming language is possible, but
+can be tricky. Using a specific language to do so can help to keep a more
+abstract mindset.
+
+Anything you write in Quint is guaranteed to be compatible with the Temporal
+Logic of Actions (TLA - the logic, not TLA+ the language), and therefore
+verifiable with a model checker. If we were to try and translate arbitrary
+programs to TLA, this would only support a fragment of the language that obeys
+certain rules of the logic. This is also true for other verification techniques,
+and that's why formal verification of generic programs is so limited.
+
+</FAQBox>
+
+<FAQBox title="How does Quint compare to static analyzers?">
+
+Quint is used to reason about behaviors of programs and how things change over
+time, and it does so by simulating or model checking executions. Static
+analyzers, on the other hand, find problems *without* any execution of the
+analyzed code, and only by looking at the code itself. A type checker is a
+static analyzer. You can also have a static analyzer that flags every time
+you write a division without checking that the divisor is not zero before -
+which doesn't necessarily mean that a division by zero will happen in runtime.
+
+If you can use a static analyzer to search for a class of errors (i.e.
+null checks), you should definitely use that. Use Quint for what you cannot do
+with a static analyzer (which is a lot!).
+
+This is also one of the reasons why Quint has a type system. Although we could
+check typing using invariants, as people often do in TLA+, we can do it
+statically with a regular type checker - and that is much better.
+
+Static analyzers won't be able to tell you if your consensus algorithm does
+consensus as you expect, but Quint will. Also, trying to use static analyzers to
+find complex problems usually results in many false positives, while model
+checking doesn't have that problem - if it finds an issue, you'll get a
+counterexample with a precise way of reproducing the problem.
+
+</FAQBox>
+
 <FAQBox title="What are spells?">
   Spells are simply Quint modules that contain often-used definitions. There is
   nothing special about these definitions. They are probably a bit more
@@ -79,7 +258,7 @@ Whenever we call `min(2, 3)`, we get `2` as a result, no matter what the values
 Impure definitions have the following important property:
 **An impure definition may produce different results for the same parameter
 values**. An impure definition **may read** the values of state variables, which
-may effect in different results.
+may affect in different results.
 
 Consider the following definitions:
 
@@ -126,7 +305,7 @@ changing with the values of `time` and `velocity`.
 A value that is defined via `pure val` is constant in the sense that it never
 changes in an execution. A `const` definition also declares a constant value.
 However, the value of `const` is not fixed at the time of specification writing,
-but it has to be fixed by instantiating the module.  
+but it has to be fixed by instantiating the module.
 
 Here is an example that illustrates the difference between `pure val` and `const`:
 

editor-plugins/highlight.js/quint.js

@@ -38,6 +38,7 @@ function quintHljs(hljs) {
         scope: 'number',
         begin: '-?(0x[0-9a-fA-F]([0-9a-fA-F]|_[0-9a-fA-F])*|0|[1-9]([0-9]|_[0-9])*)',
       },
+      hljs.SHEBANG, // file-leading hashbang
       hljs.C_LINE_COMMENT_MODE,  // single line comments
       hljs.C_BLOCK_COMMENT_MODE, // multiline comments
     ],

quint/.nvmrc

@@ -1 +1 @@
-16.11.1
+19.9.0

quint/apalache-dist-tests.md

@@ -31,7 +31,7 @@ quint verify --verbosity=1 ../examples/language-features/booleans.qnt | \
 
 <!-- !test out server not running -->
 ```
-Downloading Apalache distribution... done.
+Downloading Apalache distribution 0.46.1... done.
 [ok] No violation found (duration).
 [ok] No violation found (duration).
 ```

quint/cli-tests.md

@@ -381,3 +381,15 @@ Regression test for [#1108](https://github.com/informalsystems/quint/issues/1108
 
 <!-- !test check 1108 -->
     quint parse testFixture/_1052one.qnt
+
+### OK on typecheck SuperSpec via Unix hashbang
+
+See [#1500](https://github.com/informalsystems/quint/issues/1500).
+
+<!-- !test exit 0 -->
+<!-- !test check typecheck SuperSpec via Unix hashbang -->
+```
+if [ `uname -s` == 'Linux' -o `uname -s` == 'Darwin' ]; then
+    ./testFixture/SuperSpec.qnt
+fi
+```