diff --git a/CHANGELOG.md b/CHANGELOG.md index 938958a1a..ad6eba5a7 100644 --- a/CHANGELOG.md +++ b/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) diff --git a/evaluator/fixtures/mbt_metadata.qnt b/evaluator/fixtures/mbt_metadata.qnt new file mode 100644 index 000000000..5254bebe9 --- /dev/null +++ b/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), + } + } +} diff --git a/evaluator/src/simulator.rs b/evaluator/src/simulator.rs index ab35eede9..3e97016b8 100644 --- a/evaluator/src/simulator.rs +++ b/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 { if !init.execute(env)?.as_bool() { diff --git a/evaluator/tests/simulator_tests.rs b/evaluator/tests/simulator_tests.rs index 5e4eac6a0..60e573e80 100644 --- a/evaluator/tests/simulator_tests.rs +++ b/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");