From 2cd6b4c661c2dfee6e0f06066692d667c35c28c6 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 17 Oct 2024 10:09:40 -0300 Subject: [PATCH 1/4] Track nondet picks on cache hits as well --- quint/src/runtime/impl/builder.ts | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/quint/src/runtime/impl/builder.ts b/quint/src/runtime/impl/builder.ts index b51839663..17c2e7965 100644 --- a/quint/src/runtime/impl/builder.ts +++ b/quint/src/runtime/impl/builder.ts @@ -318,12 +318,14 @@ function buildDefCore(builder: Builder, def: LookupDefinition): EvalFunction { return ctx => { if (cachedValue.value === undefined) { cachedValue.value = bodyEval(ctx) - if (def.qualifier === 'nondet') { - cachedValue.value - .map(value => ctx.varStorage.nondetPicks.set(def.name, value)) - .mapLeft(_ => ctx.varStorage.nondetPicks.set(def.name, undefined)) - } } + + if (def.qualifier === 'nondet') { + cachedValue.value + .map(value => ctx.varStorage.nondetPicks.set(def.name, value)) + .mapLeft(_ => ctx.varStorage.nondetPicks.set(def.name, undefined)) + } + return cachedValue.value } } From 3c5fa31fdf6cd2d73bcdc24d3f9729ef3d5caf78 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 17 Oct 2024 10:17:27 -0300 Subject: [PATCH 2/4] Add regression test for the getting started spec --- quint/io-cli-tests.md | 52 +++++++++++++++++++ .../testFixture/simulator/gettingStarted.qnt | 35 +++++++++++++ 2 files changed, 87 insertions(+) create mode 100644 quint/testFixture/simulator/gettingStarted.qnt diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 27b0cb256..3f64a769d 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -482,6 +482,58 @@ Use --verbosity=3 to show executions. error: Invariant violated ``` +### Run finds invariant violation with metadata on bank spec + +Make sure the bank spec we use at the Getting Started guide has correct tracking of metadata + + +``` +output=$(quint run --seed=0xcc198528dea8b --mbt \ + --invariant=no_negatives ./testFixture/simulator/gettingStarted.qnt 2>&1) +exit_code=$? +echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*gettingStarted.qnt# HOME/gettingStarted.qnt#g' +exit $exit_code +``` + + + +``` +An example execution: + +[State 0] +{ + action_taken: "init", + balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0), + nondet_picks: { account: None, amount: None } +} + +[State 1] +{ + action_taken: "deposit", + balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("charlie"), amount: Some(53) } +} + +[State 2] +{ + action_taken: "deposit", + balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("alice"), amount: Some(26) } +} + +[State 3] +{ + action_taken: "withdraw", + balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("alice"), amount: Some(39) } +} + +[violation] Found an issue (duration). +Use --seed=0xcc198528dea8b to reproduce. +Use --verbosity=3 to show executions. +error: Invariant violated +``` + ### Run finds an example The command `run` finds an example. diff --git a/quint/testFixture/simulator/gettingStarted.qnt b/quint/testFixture/simulator/gettingStarted.qnt new file mode 100644 index 000000000..586dc4b4d --- /dev/null +++ b/quint/testFixture/simulator/gettingStarted.qnt @@ -0,0 +1,35 @@ +module bank { + /// A state variable to store the balance of each account + var balances: str -> int + + pure val ADDRESSES = Set("alice", "bob", "charlie") + + action deposit(account, amount) = { + // Increment balance of account by amount + balances' = balances.setBy(account, curr => curr + amount) + } + + action withdraw(account, amount) = { + // Decrement balance of account by amount + balances' = balances.setBy(account, curr => curr - amount) + } + + action init = { + // At the initial state, all balances are zero + balances' = ADDRESSES.mapBy(_ => 0) + } + + action step = { + // Non-deterministically pick an address and an amount + nondet account = ADDRESSES.oneOf() + nondet amount = 1.to(100).oneOf() + // Non-deterministically choose to either deposit or withdraw + any { + deposit(account, amount), + withdraw(account, amount), + } + } + + /// An invariant stating that all accounts should have a non-negative balance + val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0) +} From aa5021cf19ac9b7921d0c86692ba3ec2a7903b85 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 17 Oct 2024 10:21:32 -0300 Subject: [PATCH 3/4] Add CHANGELOG entry --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f25242d96..93a19eb7d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- Fixed a problem where using `--mbt` resulted in missing data on `nondet_picks` + due to internal caching (#1531) + ### Security ## v0.22.2 -- 2024-10-08 From 11921c4dc3d443f16a1b125329b767b6c1604367 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 28 Oct 2024 09:58:07 -0300 Subject: [PATCH 4/4] Update new test's expectation --- quint/io-cli-tests.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 2661dcd9d..d9777549f 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -529,8 +529,8 @@ An example execution: } [violation] Found an issue (duration). -Use --seed=0xcc198528dea8b to reproduce. Use --verbosity=3 to show executions. +Use --seed=0xcc198528dea8b to reproduce. error: Invariant violated ```