fix(RS): Fix stale MBT annotation on the initial state of --mbt traces

CHANGELOG.md

@@ -13,6 +13,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Removed
 ### Fixed
 
+- Fixed the Rust evaluator sometimes recording a wrong `mbt::actionTaken` and `mbt::nondetPicks` on the initial state of `--mbt` traces (#2012)
 - Fixed `--step`/`--init` resolving to a state variable instead of an action when the variable is named `step` or `init` (#1969)
 - `quint compile --target=json` no longer requires `init` and `step` to exist in the module (#1971)
 - Prevent stack overflow in `getTraceStatistics` (#1992)

evaluator/fixtures/mbt_metadata.qnt

@@ -0,0 +1,22 @@
+module mbtMetadata {
+  // Every run of this spec dead-ends: once n == 2, both picks of z disable
+  // incBy, so step evaluates to false
+
+  var n: int
+
+  def inv = n >= 0
+
+  action init = n' = 0
+
+  action incBy(z: int): bool = all {
+    n + z <= 2,
+    n' = n + z,
+  }
+
+  action step = {
+    nondet z = 1.to(2).oneOf()
+    any {
+      incBy(z),
+    }
+  }
+}

evaluator/src/simulator.rs

@@ -202,6 +202,11 @@ impl ParsedQuint {
             trace_witnessed.fill(false);
             let mut remaining = compiled_witnesses.len();
 
+            // Clear storage so that metadata left by a previous sample's
+            // failed step attempt is not recorded into this sample's initial
+            // state.
+            env.var_storage.borrow_mut().clear_metadata();
+
             // Wrap execute calls to catch panics and print seed
             let result = catch_unwind(AssertUnwindSafe(|| -> Result<bool, QuintError> {
                 if !init.execute(env)?.as_bool() {

evaluator/tests/simulator_tests.rs

@@ -184,6 +184,59 @@ fn tictactoe_n_traces_1_fast_return() {
     );
 }
 
+#[test]
+/// The initial state of every trace should be annotated with `init` and no
+/// nondet picks, even when a previous sample ended in a failed step attempt
+fn mbt_initial_state_metadata_reset() {
+    let file_path: &Path = Path::new("fixtures/mbt_metadata.qnt");
+
+    let parsed = helpers::parse_from_path(file_path, "init", "step", Some("inv"), None).unwrap();
+    let config = SimulationConfig {
+        steps: 5,
+        samples: 20,
+        n_traces: 20,
+        seed: Some(0x42),
+        store_metadata: true,
+        verbosity: Verbosity::default(),
+    };
+    let result = parsed.simulate(config, progress::no_report());
+    assert!(result.is_ok());
+    let result = result.unwrap();
+    assert!(!result.best_traces.is_empty());
+
+    for (i, trace) in result.best_traces.iter().enumerate() {
+        let state0 = &trace
+            .states
+            .first()
+            .expect("every trace should have an initial state")
+            .value;
+        let record = state0.as_record_map();
+
+        let action_taken = record
+            .get("mbt::actionTaken")
+            .expect("initial state should have mbt::actionTaken");
+        assert_eq!(
+            action_taken.as_str().as_str(),
+            "init",
+            "trace {i}: initial state labeled {:?} instead of \"init\"",
+            action_taken.as_str()
+        );
+
+        let picks = record
+            .get("mbt::nondetPicks")
+            .expect("initial state should have mbt::nondetPicks")
+            .as_record_map();
+        for (name, pick) in picks.iter() {
+            let (label, _) = pick.as_variant();
+            assert_eq!(
+                label.as_str(),
+                "None",
+                "trace {i}: initial state has leaked nondet pick for {name}"
+            );
+        }
+    }
+}
+
 #[test]
 fn tictactoe_best_traces_quality_order() {
     let file_path: &Path = Path::new("fixtures/tictactoe.qnt");