From 0f0b76e33ef6ecc150c84bb70fcad5901f83aeec Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas.pani@gmail.com>
Date: Thu, 28 Sep 2023 13:20:27 +0200
Subject: [PATCH 1/3] Add --random-transitions to run Apalache symbolic
 simulator

---
 quint/src/cli.ts         | 5 +++++
 quint/src/cliCommands.ts | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index 54b080a0f..0ca1a0634 100755
--- 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
index 7376bbe59..90e6fd082 100644
--- 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',
+      },
     },
   }
 

From d046ae96c4b34819a653122ed37ceee24ee7a698 Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas.pani@gmail.com>
Date: Thu, 28 Sep 2023 14:42:22 +0200
Subject: [PATCH 2/3] Update docs

---
 doc/quint.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/doc/quint.md b/doc/quint.md
index b60f8e99d..32b45f6f0 100644
--- 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)

From 6653ae82f34e0d9e4bafa677531a441b25ecf865 Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas.pani@gmail.com>
Date: Thu, 28 Sep 2023 14:45:23 +0200
Subject: [PATCH 3/3] Update changelog

---
 CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6dfd9570f..bae7ec32f 100644
--- 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