Merge pull request #1188 from informalsystems/th/symbsim

Add --random-transitions to run Apalache symbolic simulator
informalsystems · Sep 28, 2023 · 576d72b · 576d72b
2 parents 8b7bd64 + 6653ae8
commit 576d72b
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -8,6 +8,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- Added `--random-transitions` flag for `verify`, enabling symbolic simulation
+  through Apalache (#1188)
+
 ### Changed
 ### Deprecated
 ### Removed

diff --git a/doc/quint.md b/doc/quint.md
@@ -277,6 +277,8 @@ Options:
   --invariant        the invariants to check, separated by a comma      [string]
   --temporal         the temporal properties to check, separated by a comma
                                                                         [string]
+  --random-transitions  choose transitions at random (= use symbolic simulation)
+                                                      [boolean] [default: false]
   --apalache-config  Filename of the additional Apalache configuration (in the
                      HOCON format, a superset of JSON)                  [string]
   --verbosity        control how much output is produced (0 to 5)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
@@ -240,6 +240,11 @@ const verifyCmd = {
         type: 'string',
         coerce: (s: string) => s.split(','),
       })
+      .option('random-transitions', {
+        desc: 'choose transitions at random (= use symbolic simulation)',
+        type: 'boolean',
+        default: false,
+      })
       .option('apalache-config', {
         desc: 'Filename of the additional Apalache configuration (in the HOCON format, a superset of JSON)',
         type: 'string',

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
@@ -644,6 +644,9 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
       next: 'q::step',
       inv: args.invariant ? ['q::inv'] : undefined,
       'temporal-props': args.temporal ? ['q::temporalProps'] : undefined,
+      tuning: {
+        'search.simulation': args.randomTransitions ? 'true' : 'false',
+      },
     },
   }