Merge pull request #1662 from jesicaMao/feat/multiple-invariants-reporting

feat: Add support for multiple invariants in CLI commands

Author: bugarela

CHANGELOG.md

@@ -8,6 +8,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- `quint run` and `quint verify` can now receive multiple invariants through
+  `--invariants` and Quint prints which ones were violated in the found
+  violation (#1662)
+
 ### Changed
 
 - `--out-itf` does not suppress outputs anymore. Shown output amount only depends on `--verbosity` now (#1664) 

docs/pages/docs/checking-properties.mdx

@@ -54,12 +54,12 @@ quint run gettingStarted.qnt --witnesses=alice_more_than_bob --max-steps=5
 
 Quint reports:
 ```ansi
-[ok] No violation found (599ms).
-You may increase --max-samples and --max-steps.
-Use --verbosity to produce more (or less) output.
-Witnesses:
-alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
-Use --seed=0x1c8a2137939c73 to reproduce.
+[ok] No violation found (599ms).
+You may increase --max-samples and --max-steps.
+Use --verbosity to produce more (or less) output.
+Witnesses:
+alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
+Use --seed=0x1c8a2137939c73 to reproduce.
 ```
 
 And that informs us that, in most executions, there is a state where Alice has a larger balance than that of Bob.
@@ -78,16 +78,49 @@ quint run gettingStarted.qnt --invariant="not(alice_more_than_bob)" --max-steps=
 
 Quint reports:
 ```ansi
-An example execution:
-
-[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
-
-[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
-
-[violation] Found an issue (8ms).
-Use --verbosity=3 to show executions.
-Use --seed=0xa0bbf64f2c03 to reproduce.
-error: Invariant violated
+An example execution:
+
+[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
+
+[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
+
+[violation] Found an issue (8ms).
+Use --verbosity=3 to show executions.
+Use --seed=0xa0bbf64f2c03 to reproduce.
+error: Invariant violated
 ```
 
 Although it says "Invariant violated", this is exactly what we wanted: an example where Alice has more balance than Bob.
+
+### Using multiple invariants with `--invariants`
+
+If you want to check multiple invariants at once and determine which ones are violated, you can use the `--invariants` option:
+
+```sh
+quint run bank.qnt --invariants no_negatives accounts_match total_positive
+```
+
+Quint will check all three invariants and report which specific ones are violated:
+
+```ansi
+[90mAn example execution:[39m
+[90m[39m
+[[1mState 0[22m] { balances[90m:[39m [32mMap[39m([32m"alice"[39m[90m ->[39m [33m0[39m, [32m"bob"[39m[90m ->[39m [33m0[39m, [32m"charlie"[39m[90m ->[39m [33m0[39m) }
+
+[[1mState 1[22m] { balances[90m:[39m [32mMap[39m([32m"alice"[39m[90m ->[39m [33m-63[39m, [32m"bob"[39m[90m ->[39m [33m0[39m, [32m"charlie"[39m[90m ->[39m [33m0[39m) }
+
+[31m[violation][39m Found an issue [90m(44ms).[39m
+[31m  ❌ no_negatives[39m
+[31m  ❌ total_positive[39m
+[90mUse --verbosity=3 to show executions.[39m
+[90mUse --seed=0x4e85b3a53f7ef to reproduce.[39m
+error: Invariant violated
+```
+
+This makes it easier to identify which specific properties are being violated when you have multiple invariants to check.
+
+The `--invariants` option also works with the `verify` command, allowing you to check multiple invariants with formal verification:
+
+```sh
+quint verify bank.qnt --invariants no_negatives accounts_match total_positive
+```

docs/pages/docs/quint.md

@@ -238,8 +238,12 @@ Options:
                                                           [number] [default: 20]
   --init         name of the initializer action       [string] [default: "init"]
   --step         name of the step action              [string] [default: "step"]
-  --invariant    invariant to check: a definition name or an expression
-                                                      [string] [default: "true"]
+  --invariants   space separated list of invariants to check (definition names).
+                 When specified, all invariants are combined with AND and
+                 checked together, with detailed reporting of which ones were
+                 violated                                  [array] [default: []]
+  --invariant    invariant to check: a definition name or an expression. Can be
+                 used together with --invariants      [string] [default: "true"]
   --witnesses    space separated list of witnesses to report on (counting for
                  how many traces the witness is true)      [array] [default: []]
   --hide         space separated list of variable names to hide from the terminal
@@ -351,10 +355,13 @@ Options:
                         filename)                                       [string]
   --init                name of the initializer action[string] [default: "init"]
   --step                name of the step action       [string] [default: "step"]
-  --invariant           the invariants to check, separated by commas (e.g.)
-                                                                        [string]
+  --invariant           the invariants to check, separated by commas    [string]
   --temporal            the temporal properties to check, separated by commas
                                                                         [string]
+  --invariants          space separated list of invariants to check (definition
+                        names). When specified, all invariants are combined with
+                        AND and checked together, with detailed reporting of
+                        which ones were violated           [array] [default: []]
   --out-itf             output the trace in the Informal Trace Format to file
                         (suppresses all console output)                 [string]
   --max-steps           the maximum number of steps in every trace

quint/io-cli-tests.md

@@ -1505,3 +1505,23 @@ An example execution:
 
 [State 1]
 ```
+
+### Prints violated invariants when multiple invariants are given 
+
+<!-- !test exit 1 -->
+<!-- !test in multiple invariants -->
+```
+output=$(quint run ../examples/games/tictactoe/tictactoe.qnt --invariants="not(won(X))" "not(stalemate)" --max-samples=100 --seed=0x2b442ab439177)
+exit_code=$?
+echo "$output" | tail -n4 | sed -e 's/([0-9]*ms.*)/(duration)/g'
+exit $exit_code
+```
+
+<!-- !test out multiple invariants -->
+```
+[violation] Found an issue (duration).
+  ❌ not(won(X))
+Use --verbosity=3 to show executions.
+Use --seed=0x2b442ab439177 to reproduce.
+```
+

quint/src/cli.ts

@@ -266,8 +266,13 @@ const runCmd = {
         type: 'string',
         default: 'step',
       })
+      .option('invariants', {
+        desc: 'space separated list of invariants to check (definition names). When specified, all invariants are combined with AND and checked together, with detailed reporting of which ones were violated',
+        type: 'array',
+        default: [],
+      })
       .option('invariant', {
-        desc: 'invariant to check: a definition name or an expression',
+        desc: 'invariant to check: a definition name or an expression. Can be used together with --invariants',
         type: 'string',
         default: 'true',
       })
@@ -318,6 +323,11 @@ const verifyCmd = {
   desc: `Verify a Quint specification via Apalache`,
   builder: (yargs: any) =>
     compileOpts(yargs)
+      .option('invariants', {
+        desc: 'space separated list of invariants to check (definition names). When specified, all invariants are combined with AND and checked together, with detailed reporting of which ones were violated',
+        type: 'array',
+        default: [],
+      })
       .option('out-itf', {
         desc: 'output the trace in the Informal Trace Format to file, e.g., out.itf.json (suppresses all console output)',
         type: 'string',