Merge pull request #1531 from informalsystems/gabriela/fix-nondet-picks

Fix nondet picks not being tracked correctly in the getting started spec

CHANGELOG.md

@@ -13,6 +13,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Removed
 ### Fixed
 
+- Fixed a problem where using `--mbt` resulted in missing data on `nondet_picks`
+  due to internal caching (#1531)
 - Hashbang lines are now properly highlighted as comments in vscode and in highlight.js.
 
 ### Security

quint/io-cli-tests.md

@@ -482,6 +482,58 @@ Use --seed=0x308623f2a48e7 to reproduce.
 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
+
+<!-- !test in run finds violation with metadata on bank -->
+```
+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
+```
+
+<!-- !test exit 1 -->
+<!-- !test out run finds violation with metadata on bank -->
+```
+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 --verbosity=3 to show executions.
+Use --seed=0xcc198528dea8b to reproduce.
+error: Invariant violated
+```
+
 ### Run finds an example
 
 The command `run` finds an example.

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
       }
     }

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)
+}