fix(RS): Fix stale MBT annotation on the initial state of --mbt traces - #2012
Open
bmastenbrook wants to merge 1 commit into
Open
fix(RS): Fix stale MBT annotation on the initial state of --mbt traces#2012bmastenbrook wants to merge 1 commit into
--mbt traces#2012bmastenbrook wants to merge 1 commit into
Conversation
A sample that ends because `step` evaluated to false leaves the failed attempt's `action_taken` and `nondet_picks` in the storage. Since `track_action` is first-write-wins, the next sample's `init` could not relabel them, and its initial state was recorded with the previous sample's metadata: `mbt::actionTaken` set to the composite action's name (e.g. "step") and `mbt::nondetPicks` holding values no executed transition used. Clear the metadata registers at the start of every sample, making the sample boundary a metadata boundary regardless of how the previous sample ended. This matches the TypeScript simulator, which resets its VarStorage at the top of every run. The regression test uses a fixture that dead-ends on every sample, so every trace after a thread's first exhibits the corruption without the reset. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
bmastenbrook
force-pushed
the
fix-mbt-init-metadata
branch
from
August 13, 2026 13:17
717d54e to
5b7a850
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes #2011. When simulating with
--mbt, the Rust evaluator sometimes records the initial state of a trace withmbt::actionTakenset to the composite step action's name (e.g."step") instead of"init", and withmbt::nondetPickspopulated with values no transition in the trace used. See the issue for a minimal reproduction and full analysis.The MBT registers
action_takenandnondet_picksinStorageare cleared after a state is recorded (Env::shift) and before each candidate insideany— but never at the start of a sample. A sample that ends becausestepevaluated tofalseleaves the failed attempt's values in the registers, and sincetrack_actionis first-write-wins, the next sample'sinitcannot relabel them:shiftrecords that sample's initial state with the previous sample's stale metadata.Fix
evaluator/src/simulator.rs): clear the metadata registers at the start of every sample insimulate_with_env, so the sample boundary is a metadata boundary regardless of how the previous sample ended. This is a no-op when--mbtis not set, and matches the TypeScript simulator, which resets itsVarStorage(including MBT metadata) at the top of every run.A regression test was added (
evaluator/tests/simulator_tests.rs, with fixtureevaluator/fixtures/mbt_metadata.qnt— a spec whose every sample dead-ends): it fails before this change withinitial state labeled "step" instead of "init"and passes after. Manually verified with the issue's reproduction: 200/200 corrupted initial states before, 0/200 after; a spec with intermittent dead-ends goes from 91/100 to 0/100; non-initial annotations are unchanged (machine-checked against the state payloads).(including screenshots is helpful)
CHANGELOG.mdfor any new functionalityAI disclosure: This PR was developed with AI assistance (Claude). The fix, tests, and manual verification were reviewed by a human.