diff --git a/CHANGELOG.md b/CHANGELOG.md index 06129051c..bc0dda5f7 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/quint/cli-tests.md b/quint/cli-tests.md index ca2b6b5dd..4ca7f4ffc 100644 --- a/quint/cli-tests.md +++ b/quint/cli-tests.md @@ -327,7 +327,7 @@ fi 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 diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 2e9c9427b..8c66cf2df 100644 --- a/quint/io-cli-tests.md +++ b/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 ``` -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. ``` -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. ``` -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" } ``` diff --git a/quint/src/runtime/impl/builtins.ts b/quint/src/runtime/impl/builtins.ts index 332289b29..1864e4978 100644 --- a/quint/src/runtime/impl/builtins.ts +++ b/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':