Add regression test for the getting started spec

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
+
+<!-- !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 --seed=0xcc198528dea8b to reproduce.
+Use --verbosity=3 to show executions.
+error: Invariant violated
+```
+
 ### Run finds an example
 
 The command `run` finds an example.

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