Add generate operator

CHANGELOG.md

@@ -55,6 +55,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
+- Add the operator `generate` to mirror `Apalache!Gen` (see #1455).
 - In the `verify` command, add warning if `--out-itf` option contains `{test}` or `{seq}` as those have no effect since Apalache only produces a single trace (#1485)
 - The `run` and `test` commands now display a progress bar (#1457)
 

examples/README.md

@@ -81,6 +81,7 @@ listed without any additional command line arguments.
 | [games/tictactoe/tictactoe.qnt](./games/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/generate.qnt](./language-features/generate.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/imports.qnt](./language-features/imports.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/instances.qnt](./language-features/instances.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/language-features/generate.qnt

@@ -0,0 +1,20 @@
+// demonstrating the use of 'generate'
+module gen {
+  var S: Set[int]
+  var T: Set[{ x: int, y: bool }]
+
+  action init = {
+    nondet iS = generate(10, Set(0))
+    nondet iT = generate(20, Set({ x: 0, y: false }))
+    all {
+      S' = iS,
+      T' = iT,
+    }
+  }
+
+  action step =
+    all {
+      S' = S,
+      T' = T,
+    }
+}

quint/cli-tests.md

@@ -184,6 +184,11 @@ This example was pointing to Paxos. Now it does not typecheck.
 <!-- !test check coin - Types & Effects-->
     quint typecheck ../examples/tutorials/coin.qnt
 
+### OK on typecheck generate
+
+<!-- !test check generate - Types & Effects -->
+    quint typecheck ../examples/language-features/generate.qnt
+
 ### OK on test SimpleAuction.qnt
 
 <!-- !test check SimpleAuction - Syntax/Types & Effects/Unit tests -->

quint/src/effects/NondetChecker.ts

@@ -5,8 +5,8 @@
  * --------------------------------------------------------------------------------- */
 
 /**
- * Checking for the misuse of 'nondet' and 'oneOf'. Necessary to ensure they are
- * compatible with the exists operator from TLA+.
+ * Checking for the misuse of 'nondet', 'oneOf', and 'generate'.
+ * Necessary to ensure they are compatible with the exists operator from TLA+.
  *
  * @author Gabriela Moreira
  *
@@ -32,7 +32,7 @@ export class NondetChecker implements IRVisitor {
   }
 
   /**
-   * Checks declarations for misuse of 'nondet' and 'oneOf'.
+   * Checks declarations for misuse of 'nondet', 'oneOf', and 'generate'.
    *
    * @param types - the types of the declarations
    * @param declarations - the declarations to check
@@ -66,15 +66,15 @@ export class NondetChecker implements IRVisitor {
   }
 
   enterApp(app: QuintApp) {
-    if (app.opcode !== 'oneOf') {
+    if (app.opcode !== 'oneOf' && app.opcode !== 'generate') {
       // nothing to check
       return
     }
 
     if (this.lastDefQualifier !== 'nondet') {
       this.errors.push({
         code: 'QNT203',
-        message: `'oneOf' must be used inside a nondet definition`,
+        message: `'${app.opcode}' must be used inside a nondet definition`,
         reference: app.id,
         data: {},
       })
@@ -89,10 +89,10 @@ export class NondetChecker implements IRVisitor {
 
     // body of nondet must be an application of oneOf
     const body = expr.opdef.expr
-    if (body.kind !== 'app' || body.opcode !== 'oneOf') {
+    if (body.kind !== 'app' || (body.opcode !== 'oneOf' && body.opcode !== 'generate')) {
       this.errors.push({
         code: 'QNT204',
-        message: `'oneOf' must be the outermost expression in a nondet definition`,
+        message: `'oneOf' and 'generate' must be the outermost expressions in a nondet definition`,
         reference: body.id,
         data: {},
       })

quint/src/effects/builtinSignatures.ts

@@ -202,6 +202,7 @@ export const integerOperators = [
   { name: 'ilte', effect: standardPropagation(2) },
   { name: 'igte', effect: standardPropagation(2) },
   { name: 'to', effect: standardPropagation(2) },
+  { name: 'generate', effect: standardPropagation(2) },
 ]
 
 const temporalOperators = [

quint/src/ir/quintIr.ts

@@ -156,6 +156,7 @@ export const builtinOpCodes = [
   'foldl',
   'foldr',
   'forall',
+  'generate',
   'get',
   'head',
   'iadd',

quint/src/names/base.ts

@@ -176,6 +176,7 @@ export const builtinNames = [
   'allLists',
   'allListsUpTo',
   'chooseSome',
+  'generate',
   'oneOf',
   'isFinite',
   'size',

quint/src/quintError.ts

@@ -115,6 +115,8 @@ export type ErrorCode =
   | 'QNT513'
   /* QNT514: Cardinality is infinite */
   | 'QNT514'
+  /* QNT515: 'generate' is not supported by the simulator */
+  | 'QNT515'
 
 /* Additional data for a Quint error */
 export interface QuintErrorData {

quint/src/types/builtinSignatures.ts

@@ -106,6 +106,7 @@ const integerOperators = [
   { name: 'igte', type: '(int, int) => bool' },
   { name: 'to', type: '(int, int) => Set[int]' },
   { name: 'iuminus', type: '(int) => int' },
+  { name: 'generate', type: '(int, a) => a' },
 ]
 const temporalOperators = [
   { name: 'always', type: '(bool) => bool' },

quint/test/effects/NondetChecker.test.ts

@@ -61,7 +61,7 @@ describe('checkNondets', () => {
     assert.sameDeepMembers(errors, [
       {
         code: 'QNT204',
-        message: "'oneOf' must be the outermost expression in a nondet definition",
+        message: "'oneOf' and 'generate' must be the outermost expressions in a nondet definition",
         reference: 8n,
         data: {},
       },