Merge pull request #1582 from jff-work/main

Changed Any Operator to be less Wasteful

CHANGELOG.md

@@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 
 - Bumped Apalache to 0.47.2 (#1565)
+- Changed how an action from `any` gets picked, improving performance significantly (#1582)
 
 ### Deprecated
 ### Removed

quint/cli-tests.md

@@ -327,7 +327,7 @@ fi
 <!-- !test check gradualPonzi - Run progressInv -->
     quint run --invariant=progressInv --main=gradualPonziTest \
       --max-samples=1000 --max-steps=50 \
-      --seed=0xa7bf730b93981 \
+      --seed=0x18df4a4a4f958b \
       ../examples/solidity/GradualPonzi/gradualPonzi.qnt
 
 ### FAIL on run gradualPonzi::noLeftoversInv

quint/io-cli-tests.md

@@ -444,7 +444,7 @@ An example execution:
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x308623f2a48e7 to reproduce.
+Use --seed=0x308623f2a4957 to reproduce.
 error: Invariant violated
 ```
 
@@ -454,7 +454,7 @@ The command `run` finds an invariant violation and outputs metadata for MBT, whe
 
 <!-- !test in run finds violation with metadata -->
 ```
-output=$(quint run --seed=0x308623f2a48e7 --mbt --max-steps=4 \
+output=$(quint run --seed=0x308623f2a4957 --mbt --max-steps=4 \
   --invariant='n < 10' ../examples/language-features/counters.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*counters.qnt#      HOME/counters.qnt#g'
@@ -478,7 +478,7 @@ An example execution:
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x308623f2a48e7 to reproduce.
+Use --seed=0x308623f2a4957 to reproduce.
 error: Invariant violated
 ```
 
@@ -509,23 +509,9 @@ An example execution:
 
 [State 1]
 {
-  balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53),
-  mbt::actionTaken: "deposit",
-  mbt::nondetPicks: { account: Some("charlie"), amount: Some(53) }
-}
-
-[State 2]
-{
-  balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53),
-  mbt::actionTaken: "deposit",
-  mbt::nondetPicks: { account: Some("alice"), amount: Some(26) }
-}
-
-[State 3]
-{
-  balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53),
+  balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> -75),
   mbt::actionTaken: "withdraw",
-  mbt::nondetPicks: { account: Some("alice"), amount: Some(39) }
+  mbt::nondetPicks: { account: Some("charlie"), amount: Some(75) }
 }
 
 [violation] Found an issue (duration).
@@ -553,11 +539,11 @@ An example execution:
 
 [State 1] { n: 2 }
 
-[State 2] { n: 3 }
+[State 2] { n: 1 }
 
-[State 3] { n: 6 }
+[State 3] { n: 2 }
 
-[State 4] { n: 12 }
+[State 4] { n: 3 }
 
 [ok] No violation found (duration).
 You may increase --max-samples and --max-steps.
@@ -592,7 +578,7 @@ The command `run` finds an overflow in Coin.
 
 <!-- !test in run finds overflow -->
 ```
-output=$(quint run --max-steps=5 --seed=0x1e352e160ffa12 --invariant=totalSupplyDoesNotOverflowInv \
+output=$(quint run --max-steps=5 --seed=0x1e352e160ffb15 --invariant=totalSupplyDoesNotOverflowInv \
   ../examples/tutorials/coin.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*coin.qnt#      HOME/coin.qnt#g'
@@ -615,12 +601,12 @@ An example execution:
 {
   balances:
     Map(
-      "alice" -> 0,
+      "alice" ->
+        94541396474536885635239092281406920580729946306097367569491485195445962194366,
       "bob" -> 0,
       "charlie" -> 0,
       "eve" -> 0,
-      "null" ->
-        47468303772350480796754932551497789850659553878128630540503207933116325625281
+      "null" -> 0
     ),
   minter: "alice"
 }
@@ -629,20 +615,20 @@ An example execution:
 {
   balances:
     Map(
-      "alice" -> 0,
-      "bob" -> 0,
+      "alice" ->
+        94541396474536885635239092281406920580729946306097367569491485195445962194366,
+      "bob" ->
+        53481678647226234506653603827987361074517460680431655489916483293654777859474,
       "charlie" -> 0,
-      "eve" ->
-        86701019854146491074035808072771270690110858489697827845755906419340818387504,
-      "null" ->
-        47468303772350480796754932551497789850659553878128630540503207933116325625281
+      "eve" -> 0,
+      "null" -> 0
     ),
   minter: "alice"
 }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x1e352e160ffbb3 to reproduce.
+Use --seed=0x1e352e160ffb15 to reproduce.
 error: Invariant violated
 ```
 
@@ -652,7 +638,7 @@ The command `run` finds an overflow in Coin and shows the operator calls.
 
 <!-- !test in run shows calls -->
 ```
-output=$(quint run --max-steps=5 --seed=0x1786e678d45fe0 \
+output=$(quint run --max-steps=5 --seed=0x1786e678d460ed \
   --invariant=totalSupplyDoesNotOverflowInv \
   --verbosity=3 \
   ../examples/tutorials/coin.qnt 2>&1)
@@ -681,18 +667,14 @@ q::initAndInvariant => true
 [Frame 1]
 q::stepAndInvariant => true
 ├─ step => true
-│  └─ mint(
+│  └─ send(
 │       "alice",
-│       "eve",
-│       33944027745092921485394061592130395256199599638916782090017603421409072478812
-│     ) => true
-│     ├─ require(true) => true
-│     └─ require(true) => true
-│        └─ isUInt(
-│             33944027745092921485394061592130395256199599638916782090017603421409072478812
-│           ) => true
+│       "null",
+│       78071281284846825193495013785477188646129629244112530489195111677146856342020
+│     ) => false
+│     └─ require(false) => false
 └─ isUInt(
-     33944027745092921485394061592130395256199599638916782090017603421409072478812
+     78071281284846825193495013785477188646129629244112530489195111677146856342020
    ) => true
 
 [State 1]
@@ -702,79 +684,44 @@ q::stepAndInvariant => true
       "alice" -> 0,
       "bob" -> 0,
       "charlie" -> 0,
-      "eve" ->
-        33944027745092921485394061592130395256199599638916782090017603421409072478812,
-      "null" -> 0
+      "eve" -> 0,
+      "null" ->
+        78071281284846825193495013785477188646129629244112530489195111677146856342020
     ),
   minter: "alice"
 }
 
 [Frame 2]
-q::stepAndInvariant => true
-├─ step => true
-│  └─ mint(
-│       "alice",
-│       "eve",
-│       37478542505835205046968520025158070945751003972871720238447843997511300995974
-│     ) => true
-│     ├─ require(true) => true
-│     └─ require(true) => true
-│        └─ isUInt(
-│             71422570250928126532362581617288466201950603611788502328465447418920373474786
-│           ) => true
-└─ isUInt(
-     71422570250928126532362581617288466201950603611788502328465447418920373474786
-   ) => true
-
-[State 2]
-{
-  balances:
-    Map(
-      "alice" -> 0,
-      "bob" -> 0,
-      "charlie" -> 0,
-      "eve" ->
-        71422570250928126532362581617288466201950603611788502328465447418920373474786,
-      "null" -> 0
-    ),
-  minter: "alice"
-}
-
-[Frame 3]
 q::stepAndInvariant => false
 ├─ step => true
-│  └─ mint(
+│  └─ send(
 │       "alice",
-│       "null",
-│       109067983118832076063755963802104322727953985633488183463930115464609414175363
-│     ) => true
-│     ├─ require(true) => true
-│     └─ require(true) => true
-│        └─ isUInt(
-│             109067983118832076063755963802104322727953985633488183463930115464609414175363
-│           ) => true
+│       "charlie",
+│       71516992819340132902114648681722204450273946921092387316973942850220744245470
+│     ) => false
+│     └─ require(false) => false
 └─ isUInt(
-     180490553369760202596118545419392788929904589245276685792395562883529787650149
+     149588274104186958095609662467199393096403576165204917806169054527367600587490
    ) => false
 
-[State 3]
+[State 2]
 {
   balances:
     Map(
       "alice" -> 0,
       "bob" -> 0,
-      "charlie" -> 0,
-      "eve" ->
-        71422570250928126532362581617288466201950603611788502328465447418920373474786,
+      "charlie" ->
+        71516992819340132902114648681722204450273946921092387316973942850220744245470,
+      "eve" -> 0,
       "null" ->
-        109067983118832076063755963802104322727953985633488183463930115464609414175363
+        78071281284846825193495013785477188646129629244112530489195111677146856342020
     ),
   minter: "alice"
 }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x1786e678d460fe to reproduce.
+Use --seed=0x1786e678d460ed to reproduce.
 error: Invariant violated
 ```
 
@@ -833,7 +780,7 @@ rm out-itf-mbt-example.itf.json
       [
         "charlie",
         {
-          "#bigint": "49617995555028370892926474303042238797407019137772330780016167115018841762373"
+          "#bigint": "79626045751699704635016553258820412024546765398372583361896346889345270192783"
         }
       ],
       [
@@ -855,7 +802,7 @@ rm out-itf-mbt-example.itf.json
     "amount": {
       "tag": "Some",
       "value": {
-        "#bigint": "49617995555028370892926474303042238797407019137772330780016167115018841762373"
+        "#bigint": "79626045751699704635016553258820412024546765398372583361896346889345270192783"
       }
     },
     "receiver": {
@@ -864,10 +811,10 @@ rm out-itf-mbt-example.itf.json
     },
     "sender": {
       "tag": "Some",
-      "value": "bob"
+      "value": "eve"
     }
   },
-  "minter": "bob"
+  "minter": "eve"
 }
 ```
 

quint/src/runtime/impl/builtins.ts

@@ -140,55 +140,53 @@ export function lazyBuiltinLambda(
       }
 
     case 'actionAny': {
-      // Executes any of the given actions.
-      // First, we filter actions so that we only consider those that are enabled.
-      // Then, we use `rand()` to pick one of the enabled actions.
+      // Executes the first enabled action from a randomized list of actions.
+      // Returns false if no enabled actions are found.
       const app: QuintApp = { id: 0n, kind: 'app', opcode: 'actionAny', args: [] }
       return (ctx, args) => {
         const nextVarsSnapshot = ctx.varStorage.snapshot()
 
-        const evaluationResults = args.map((arg, i) => {
-          // on `any`, we reset the action taken as the goal is to save the last
-          // action picked in an `any` call
+        // Create array of indices and shuffle them
+        const indices = Array.from(args.keys())
+        // Fisher-Yates shuffle algorithm
+        for (let i = indices.length - 1; i > 0; i--) {
+          const j = Number(ctx.rand(BigInt(i + 1)))
+          // Swap: indices[i] <--> indices[j]
+          ;[indices[i], indices[j]] = [indices[j], indices[i]]
+        }
+
+        // Try actions in shuffled order until we find one that's enabled
+        for (const i of indices) {
+          // Reset state for each attempt
           ctx.varStorage.actionTaken = undefined
           ctx.varStorage.nondetPicks.forEach((_, key) => {
             ctx.varStorage.nondetPicks.set(key, undefined)
           })
 
           ctx.recorder.onAnyOptionCall(app, i)
-          const result = arg(ctx).map(result => {
-            // Save vars
-            const successor = ctx.varStorage.snapshot()
-
-            return result.toBool() ? [{ snapshot: successor, index: i }] : []
-          })
+          const result = args[i](ctx)
           ctx.recorder.onAnyOptionReturn(app, i)
 
-          return result
-        })
+          if (result.isLeft()) {
+            return result
+          }
 
-        const processedResults = mergeInMany(evaluationResults)
-          .map(suc => suc.flat())
-          .mapLeft(errors => errors[0])
-
-        return processedResults.map(potentialSuccessors => {
-          switch (potentialSuccessors.length) {
-            case 0:
-              ctx.recorder.onAnyReturn(args.length, -1)
-              ctx.varStorage.recoverSnapshot(nextVarsSnapshot)
-              return rv.mkBool(false)
-            case 1:
-              ctx.recorder.onAnyReturn(args.length, potentialSuccessors[0].index)
-              ctx.varStorage.recoverSnapshot(potentialSuccessors[0].snapshot)
-              return rv.mkBool(true)
-            default: {
-              const choice = Number(ctx.rand(BigInt(potentialSuccessors.length)))
-              ctx.recorder.onAnyReturn(args.length, potentialSuccessors[choice].index)
-              ctx.varStorage.recoverSnapshot(potentialSuccessors[choice].snapshot)
-              return rv.mkBool(true)
-            }
+          if (result.value.toBool()) {
+            // Found an enabled action - record it and return true
+            const successor = ctx.varStorage.snapshot()
+            ctx.recorder.onAnyReturn(args.length, i)
+            ctx.varStorage.recoverSnapshot(successor)
+            return right(rv.mkBool(true))
           }
-        })
+
+          // Reset state before trying next action
+          ctx.varStorage.recoverSnapshot(nextVarsSnapshot)
+        }
+
+        // No enabled actions found
+        ctx.recorder.onAnyReturn(args.length, -1)
+        ctx.varStorage.recoverSnapshot(nextVarsSnapshot)
+        return right(rv.mkBool(false))
       }
     }
     case 'actionAll':