Fest: scenario coverage, feedback-search fidelity, and pluggable timeline representations (+ evaluation)#985
Merged
Merged
Conversation
…e monitor
Adds a top-level `scenario Name observes {..} { ..states.. }` construct that
compiles to a P spec monitor carrying a coverage flag. A scenario reuses all
spec-monitor machinery (state codegen incl. hot/cold, observes validation,
send/announce forbidding, monitorMap wiring, `assert`-based attachment) but:
- is registered as a coverage monitor (PModule.coverageMonitors), and
- is EXEMPT from the end-of-run liveness check — an unsatisfied scenario left
in a hot state is "uncovered", not a liveness bug.
Its accepting (cold) state marks the scenario satisfied; the runtime already
surfaces monitor state transitions via OnMonitorStateTransition, which a later
observer will use to count satisfaction (scenario coverage) and feed compliance
into the feedback-guided search.
Compiler: SCENARIO token; scenarioMachineDecl (mirrors specMachineDecl);
Machine.IsScenario (implies IsSpec); Scope.Put + stub/decl visitors;
WriteInitializeMonitorMap emits PModule.coverageMonitors registration.
Runtime: PModule.coverageMonitors; ControlledRuntime skips the liveness check
for coverage monitors. Reserved keyword `scenario` documented.
Follow-ups (same cluster): ScenarioComplianceObserver (D2), scenario-coverage
metric in TestReport (D3), compliance -> feedback priority (D4).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…nd report Builds on the D1 `scenario` keyword to make scenario coverage observable end to end: - Auto-attach (PCheckerCodeGenerator): every scenario is added to each test/impl monitor map (observing all machines) — scenarios need no `assert`. - ScenarioComplianceObserver: an IControlledRuntimeLog that flags a scenario satisfied when its coverage monitor enters an accepting (cold) state (OnMonitorStateTransition, isInHotState == false). - TestReport: per-scenario trigger counts + distinct satisfying timelines, with Merge (sum counts, union timelines) and an "N Scenario coverage:" section in GetText that lists every declared scenario — including 0-coverage ones, which are the coverage gaps worth surfacing. - TestingEngine: creates/registers the observer per iteration and records satisfaction keyed by the schedule's abstract timeline. - Monitor.CheckLivenessTemperature: also exempts coverage monitors (completes the liveness exemption alongside the end-of-run check), so an uncovered scenario stuck in a hot state never reports a false liveness bug. Tests: - RegressionTests/.../Correct/ScenarioCoverageBasic: end-to-end — a satisfied scenario and an uncovered one; the run exits cleanly (exemption works). - UnitTests/ScenarioCoverageTest: trigger counting, unique-timeline dedup, uncovered-scenario tracking, cross-worker merge, and report text. Verified with `p check -i 200`: reports ReadAfterWrite: triggered in 199 schedules, 1 unique satisfying timeline NeverCovered: triggered in 0 schedules, 0 unique satisfying timelines Follow-up: feed compliance into feedback-guided priority (D4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…h steering Extends scenario coverage with the "how close did we get" signal and uses it to guide exploration: - Compile-time check (MachineChecker): warn when a `scenario` has no accepting (cold) state — it could never be satisfied and would always report 0. - Partial coverage: the compiler emits each scenario's total state count (PModule.scenarioStateCounts); ScenarioComplianceObserver tracks the distinct states each scenario reaches per schedule; TestReport records the best (max) partial progress and reports "best partial progress: X/Y states" for scenarios that were never fully satisfied — surfacing how close a coverage gap is, not just that it exists. - D4 (steer search): the observer computes a per-run compliance in [0,1] (max partial-progress fraction across scenarios); FeedbackGuidedStrategy boosts saved-generator priority by diversity x (1 + compliance), nudging exploration toward under-covered scenarios. With no scenario, compliance is 0 so priority == diversity (unchanged). A boost (vs the paper's strict product) avoids discarding diverse-but-scenario-irrelevant schedules, since scenarios are always auto-attached here. Tests: ScenarioCoverageTest gains partial-progress + merge-of-progress cases (6 total). Verified via `p check`: NeverCovered: triggered in 0 schedules, 0 unique satisfying timelines (best partial progress: 1/2 states) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
P runs one test case per `p check`, so suite-wide scenario coverage requires aggregating across runs. Each run now writes a machine-readable artifact (<name>[_<testcase>]_scenario_coverage.json) with per-scenario triggers, unique satisfying timelines, and best partial progress. ScenarioCoverageMerger reads a directory of these and produces a unified report: per scenario, the total triggers and unique satisfying timelines summed across test cases, how many test cases covered it (K/N), and the best partial progress anywhere — so a scenario uncovered across the whole suite stands out. - ScenarioCoverageMerger: FromReport/Write (per-run artifact) + Merge/MergeDirectory (aggregate). - TestingProcess.EmitTestReport writes the artifact when scenarios exist. - ScenarioCoverageTest gains a cross-test-case aggregation test (7 total). Follow-up: expose MergeDirectory via a CLI subcommand (the API + artifacts are in place). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…imelines, ~5-int mutation Brings the feedback-guided search closer to the paper's algorithm: - B1: ComputeDiversity now returns 1 - Jaccard(new, closest prior) in [0,1] (estimated via MinHash), instead of the unnormalized (50 - maxSim) + 20. The ordering priority and the integer mutation budget are decoupled (GeneratorRecord.Priority vs .MutationBudget), so the [0,1] metric no longer doubles as the budget; budget is proportional to novelty. Composes with the D4 compliance boost: priority = diversity x (1 + compliance). - B2: the abstract Lamport timeline keys on the receiver machine INSTANCE (id.Name) rather than its type, matching the paper's per-receiver <M,e1,e2>. - B3: mutation changes ~5 integers on average (5 sites of size 1) instead of ~25 (5 sites of ~5), keeping mutated schedules similar-but-distinct. Validation: builds clean; full regression suite green (correctness — the default non-feedback strategies are unaffected). Search-quality sanity check on TwoPhaseCommit/feedbackpct (seed 1) found the same pre-existing liveness bug in fewer schedules than pre-B (48 vs 183), consistent with the iterations-to-bug improvement this cluster targets. A full multi-seed coverage benchmark across the model corpus remains future work before flipping this on by default. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…erge Makes the cross-test-case unified report usable end to end: - MergeDirectory now recurses subdirectories, because the checker writes each run's artifact into its own output subdir (e.g. PCheckerOutput/BugFinding*/). - New `p merge-scenario-coverage [dir]` command prints the unified suite-wide report (defaults to the current directory). - ScenarioCoverageTest: file-based recursive-merge test (8 total). Validated on the ClientServer tutorial: two test cases produced artifacts and `p merge-scenario-coverage` reported WithdrawThenResponse: covered in 2/2 test cases, 597 total triggers, 32 unique satisfying timelines TwoResponses: covered in 2/2 test cases, 591 total triggers, 30 unique satisfying timelines Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Adds Fest “scenario coverage” support end-to-end (new scenario monitor syntax, runtime accounting, per-run artifacts + suite merger, and CLI command) and updates the feedback-guided search to match the paper’s Cluster B diversity/timeline/mutation behavior more closely.
Changes:
- Introduces a new
scenario Name observes {..} { ..states.. }top-level construct compiled as a spec-like monitor flagged as “coverage”, auto-attached to tests, and exempt from liveness checks. - Records per-schedule scenario satisfaction + partial progress into
TestReport, emits*_scenario_coverage.jsonartifacts, and adds a merger (p merge-scenario-coverage) for suite-wide reporting. - Refines feedback-guided search: normalized diversity score (
1 - Jaccard), instance-based timeline identity, and smaller mutation deltas.
Reviewed changes
Copilot reviewed 22 out of 24 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| Tst/UnitTests/ScenarioCoverageTest.cs | Unit tests for scenario coverage accounting, merging, and reporting. |
| Tst/RegressionTests/Feature1SMLevelDecls/Correct/ScenarioCoverageBasic/ScenarioCoverageBasic.p | End-to-end regression fixture for auto-attach + liveness exemption behavior. |
| Src/PCompiler/PCommandLine/CommandLine.cs | Adds merge-scenario-coverage CLI command wiring. |
| Src/PCompiler/CompilerCore/TypeChecker/Scope.cs | Registers scenario declarations as machines in scope. |
| Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs | Adds warning for scenarios without an accepting (cold) state. |
| Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs | Type-checks scenario declarations similarly to spec monitors. |
| Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs | Adds stub pass support for scenario declarations. |
| Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs | Flags scenario monitors (IsScenario) and treats them as spec-like monitors (IsSpec). |
| Src/PCompiler/CompilerCore/Parser/PParser.g4 | Adds scenarioMachineDecl grammar production. |
| Src/PCompiler/CompilerCore/Parser/PLexer.g4 | Adds scenario keyword token. |
| Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs | Auto-attaches scenarios to monitor maps and emits runtime metadata for coverage/liveness exemption. |
| Src/PChecker/CheckerCore/Testing/TestingProcess.cs | Writes per-test-case scenario coverage artifacts. |
| Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs | Stores scenario trigger counts, unique satisfying timelines, and partial progress; prints in report text. |
| Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs | Hooks per-iteration scenario observer and records per-schedule scenario coverage into TestReport. |
| Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IFeedbackGuidedStrategy.cs | Extends observation hook to include scenario compliance. |
| Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/ControlledRandom.cs | Adjusts mutation magnitude to ~5 ints (paper-aligned). |
| Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs | Normalizes diversity metric, separates priority from mutation budget, and boosts priority by scenario compliance. |
| Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs | Keys abstract timeline on receiver instance (id.Name) and maintains MinHash-based diversity support. |
| Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/ScenarioComplianceObserver.cs | New per-iteration observer for scenario satisfaction + partial progress. |
| Src/PChecker/CheckerCore/SystematicTesting/ScenarioCoverageMerger.cs | New JSON artifact writer + recursive directory merger for suite-wide scenario coverage reports. |
| Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs | Exempts coverage monitors from end-of-run hot-state liveness check. |
| Src/PChecker/CheckerCore/Runtime/Specifications/Monitor.cs | Exempts coverage monitors from temperature-based liveness checks. |
| Src/PChecker/CheckerCore/Runtime/PModule.cs | Adds global runtime metadata for coverage monitors + per-scenario total state counts. |
| CLAUDE.md | Documents scenario as a reserved keyword. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+32
to
+56
| public ScenarioComplianceObserver() | ||
| { | ||
| _coverageMonitorNames = PModule.coverageMonitors.Select(t => t.FullName).ToHashSet(); | ||
| AllScenarioNames = _coverageMonitorNames.Select(ShortName).ToList(); | ||
| foreach (var kv in PModule.scenarioStateCounts) | ||
| { | ||
| _totalStates[ShortName(kv.Key.FullName)] = kv.Value; | ||
| } | ||
| } | ||
|
|
||
| /// <summary>Scenarios (by short name) satisfied at least once during this iteration.</summary> | ||
| public IReadOnlyCollection<string> SatisfiedScenarios => _satisfied; | ||
|
|
||
| /// <summary>Short names of all declared scenarios (so 0-coverage ones are reported too).</summary> | ||
| public IReadOnlyCollection<string> AllScenarioNames { get; } | ||
|
|
||
| /// <summary>True if any scenario monitors are active for this run.</summary> | ||
| public bool HasScenarios => _coverageMonitorNames.Count > 0; | ||
|
|
||
| /// <summary>Distinct states <paramref name="scenario"/> entered this iteration.</summary> | ||
| public int StatesReached(string scenario) => _statesReached.TryGetValue(scenario, out var s) ? s.Count : 0; | ||
|
|
||
| /// <summary>Total states declared in <paramref name="scenario"/> (0 if unknown).</summary> | ||
| public int TotalStates(string scenario) => _totalStates.TryGetValue(scenario, out var n) ? n : 0; | ||
|
|
Member
Author
There was a problem hiding this comment.
Fixed in d287465. The observer no longer snapshots PModule in its constructor — it lazily re-reads via Refresh() whenever PModule.coverageMonitors has grown (populated by the generated InitializeMonitorMap, which runs after the observer is constructed). Verified end-to-end: a p check -s 1 run now reports scenario coverage and emits the *_scenario_coverage.json artifact (both were previously dropped on the first/only schedule).
Comment on lines
+80
to
+86
| public void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) | ||
| { | ||
| if (!isEntry || !_coverageMonitorNames.Contains(monitorType)) | ||
| { | ||
| return; | ||
| } | ||
| var scenario = ShortName(monitorType); |
Member
Author
There was a problem hiding this comment.
Fixed in d287465. OnMonitorStateTransition now calls Refresh() first, so coverage monitors registered after construction — including the initial state-entry logged during RegisterMonitor — are classified for partial-progress/satisfaction.
Comment on lines
523
to
536
| foreach (var monitor in monitorMap.Keys) | ||
| { | ||
| context.WriteLine(output, $"runtime.RegisterMonitor<{context.Names.GetNameForDecl(monitor)}>();"); | ||
| // Scenario monitors are coverage monitors: register them so the runtime | ||
| // counts their satisfaction and exempts them from the liveness check. | ||
| if (monitor.IsScenario) | ||
| { | ||
| var monitorName = context.Names.GetNameForDecl(monitor); | ||
| context.WriteLine(output, $"PModule.coverageMonitors.Add(typeof({monitorName}));"); | ||
| // Total state count enables partial-coverage reporting (states reached / total). | ||
| context.WriteLine(output, | ||
| $"PModule.scenarioStateCounts[typeof({monitorName})] = {monitor.AllStates().Count()};"); | ||
| } | ||
| } |
Member
Author
There was a problem hiding this comment.
Fixed in d287465. InitializeMonitorMap now emits PModule.coverageMonitors.Add(...) / scenarioStateCounts[...] before runtime.RegisterMonitor<...>(), so the monitor's start-state entry (logged during RegisterMonitor) is classifiable. Confirmed by partial progress now including the start state — e.g. an unsatisfiable scenario reports 2/4 states even on a -s 1 run.
Adds eval/fest-scenario-coverage/ (non-project, so CI ignores it):
- scenarios/{ClientServer,TwoPhaseCommit,Paxos}/Scenarios.p — documented example
`scenario` monitors spanning common / payload-dependent / rare-ordering /
impossible-partial behaviors (double as usage examples).
- Fest-eval-report.md — empirical evaluation across 3 models x 4 strategies
(random, feedback, feedbackpos, feedbackpct) x multi-seed, using the feature's
own coverage metrics.
- README.md — reproduction steps.
Findings: scenario coverage (full + partial), the liveness exemption, and
same-seed reproducibility all validated; feedback+PCT dominates rare-scenario
coverage and reaches first coverage at far smaller budgets; random is the most
reliable first-bug finder while feedback variants amplify a found bug (~25x more
buggy schedules); and the D4 compliance term is currently inert (saturates at
1.0 because a common scenario is always satisfied) — a one-line fix is proposed.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…mendation D4 fix — the scenario "compliance" term that steers the feedback search was a latent no-op: it was the max over ALL auto-attached scenarios of statesReached/totalStates, which saturates at 1.0 whenever any common scenario is satisfied (essentially every schedule), so priority = diversity*(1+1) was a constant factor that could not re-order saved generators (ablation: on/off byte-identical in all 60 configs). Replace it with a sparse coverage-NOVELTY signal (ScenarioSteering.NoveltyCompliance): a schedule earns compliance 1.0 only if it first-satisfies a scenario or advances the furthest state of a not-yet-satisfied scenario beyond the suite's best so far; else 0.0. It cannot saturate (a scenario stops contributing once it plateaus, incl. an unsatisfiable one at its ceiling). Compliance is now computed inside the strategy AFTER the timeline-diversity discard gate and owns its suite-state, so a discarded (timeline-redundant) schedule can no longer consume a scenario's novelty and starve a later kept schedule (a blocker surfaced by adversarial review of the first cut). Removes the old saturating RunCompliance(); adds a pure, unit-tested NoveltyCompliance helper (5 new tests). Also: surface --sch-feedbackpct as the recommended feedback strategy in the CLI help (it is the all-rounder in the evaluation); update eval/Fest-eval-report.md (reframed to lead with the feedback+PCT coverage/amplification wins) and its E6 section with the post-fix ablation (steering now measurably re-orders exploration — 4/60 configs shift — though the coverage payoff on tutorial-scale models is still negligible; value to be shown at scale). Full Release regression green (744/744, incl. 5 new steering tests). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The feedback search's diversity signal (TimelineObserver) used a per-receiver, event-TYPE, ordered-pair set — a local projection with no cross-machine causality that saturates quickly, ignoring the vector clocks the runtime already maintains. Introduce a pluggable ITimelineRepresentation (--timeline-repr), default unchanged: - pairwise (default): the historical local type-pair set. The token layout is byte-compatible with the legacy hash, so default search behavior is preserved exactly (verified: --timeline-repr pairwise == no flag; regression 756/756). - kgram: per-receiver contiguous k-grams (--timeline-kgram N, default 3) — finer, less saturation. - causal: the happens-before partial order over deliveries (from the runtime's vector clocks + per-receiver program order) abstracted to labels — the first real consumer of the already-computed clocks. - hybrid: union of causal + kgram. Plus --timeline-payload to enrich event labels with a stable payload hash. TimelineObserver keeps the shared FNV-1a + fixed-coefficient MinHash; only the token content changes. Correctness fixes surfaced by adversarial review: - VectorTime.CompareTo iterated only this.Clock.Keys, so a machine present only in the other clock was never compared — a genuine happens-before could be misreported as concurrent. Now ranges over the union of both clocks' keys (corrected the inverted doc comment too). - PSet/PMap.ToString now iterate in a deterministic (sorted) order, so --timeline-payload is reproducible under a fixed --seed. Tests: Tst/UnitTests/TimelineRepresentationTest.cs (12). Full Release suite green (756/756). Bake-off (eval/fest-scenario-coverage/Timeline-representation.md): kgram lifts coverage across models; causal takes first-bug reliability from 5/10 to 9/10 seeds (fixes feedback's get-stuck failure) but is coarse for request-response models; pairwise is dominated. Default stays pairwise. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Replace the 10-seed pilot bake-off with a larger, parallelized run (20 seeds for coverage, 40 for the discriminating bug case) plus two --timeline-payload variants, and rewrite the conclusions after an independent audit of the raw CSVs. Key corrections vs the pilot (honesty matters here): - The pilot's "causal 9/10" bug-finding regressed to 28/40 = 70% vs pairwise 45% (Fisher's exact p=0.041) — significant but MARGINAL (overlapping 95% CIs); causal's real edge is being censored less often (30% vs 55% hit the 3000 cap), not finding bugs faster. - "kgram/hybrid beat pairwise on coverage" holds in 4/5 configs, NOT universally: on TPC/NoFailure pairwise beats both and causal is top. - causal is best coverage on TPC/NoFailure yet collapses to ~1.4 timelines on ClientServer (type-level happens-before is schedule-invariant for request/response) — workload-dependent, not a clean coverage-vs-bugs trade. - --timeline-payload (whole-payload hashing) degenerates: causal+P == hybrid+P row-for-row at a constant 51, and worst at bug-finding — the "too fine" mode; needs selective-field hashing. Caveats stated plainly: one real bug on one discriminating test case, heavy censoring, tutorial-scale models. Directional, replication-worthy — not a mandate to flip the default (stays pairwise). Harness: fest-eval/run.py e8 (parallel). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Redesign the two coverage report surfaces for scannability (no metric changes):
- Per-run (TestReport.GetText): lead with a summary count ("K/N scenarios covered
(M gaps)"), then covered scenarios marked [covered], then coverage gaps marked
[ GAP ] last (with best partial progress) so gaps stand out instead of being
buried among "0 schedules" counters.
- Unified merge (ScenarioCoverageMerger.Merge): a summary line, covered vs gap
grouping, and — new — the list of WHICH test cases cover each scenario
(e.g. "covered in 2/2 test cases (tcSingleClient, tcMultipleClients)"); gaps
read "never covered in any of N test cases; best progress anywhere X/Y states".
ASCII-only markers (portable terminals); the machine-readable *_scenario_coverage.json
artifact is unchanged. Tests updated/added in ScenarioCoverageTest (summary count,
covered-before-gaps ordering, covering-test-case list). Full Release suite green (757).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… correction) Larger study: 4 known bugs (Paxos quorum-off-by-one, TPC premature-commit, TPC natural Progress liveness, ClientServer trivial) across 3 protocols, feedback reprs vs a plain --sch-random reference, 50 seeds / cap 10000; plus coverage on 4 models including the larger Raft. Independently audited from the raw CSVs. Key correction to the earlier writeup: with random in the comparison, "causal is the best bug-finder" DOES NOT HOLD. Plain random dominates every feedback variant on every bug (safety 4-5x faster; liveness fastest + 100% found). The timeline representation only re-orders feedback INTERNALLY: on the one discriminating liveness bug causal is strongest (94%, sig > kgram p<0.001; modest over pairwise/hybrid) and kgram weakest (56%); for safety bugs the repr is immaterial (identical medians). Coverage is model-dependent and does not generalize: causal worst on small models, best (but high-variance) on TPC/Raft; kgram/hybrid the reverse. Default stays pairwise. Also refreshes the E5 section with the redesigned, understandable per-run + merge report output. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ankushdesai
changed the title
The output layout was PCheckerOutput/<Mode>/ shared across all test cases, with whole-directory history rotation (<Mode>0..9). That made multi-test-case runs flaky: running -tc A then -tc B pushed A's entire output into the rotated history; the rotation Directory.Move races if different test cases run concurrently in the same root; and merge-scenario-coverage (which recurses) double-counted a test case whenever it was re-run (its artifact then exists in both <Mode>/ and <Mode>0/). Fix (single change site in CheckerConfiguration.SetOutputDirectory): group output by test case — PCheckerOutput/<testCase>/<Mode>/ — so rotation/history is per test case, concurrent runs of different test cases no longer share a directory, and "the latest run of test case X" is unambiguous (the non-numbered <Mode>/ dir). A single anonymous test (no -tc) keeps the old layout. Test-case names are path-sanitized. Complementary read-side fix: ScenarioCoverageMerger.MergeDirectory now keeps only the LATEST artifact per test case (by write time), so re-runs and rotated-history copies never double-count in the unified report. Tests: SetOutputDirectory_GroupsOutputByTestCase and MergeDirectory_DedupesReRunsOfSameTestCaseKeepingLatest. Verified end-to-end (re-run of one test case rotates only its own folder; merge still reports it once). Full Release suite green (759). No test pinned the old path. (PEx/symbolic --outdir is unchanged.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… (review) Addresses the Copilot review: scenario coverage was dropped for the first schedule (and thus for any single-schedule run — no accounting, no artifact), and the monitor's initial state-entry was missed, hurting partial-progress reporting. Root cause was a timing/ordering mismatch: - ScenarioComplianceObserver snapshotted PModule.coverageMonitors/scenarioStateCounts in its constructor, but those statics are populated by the generated InitializeMonitorMap during test setup — AFTER the observer is constructed. So iteration 1 saw an empty set. - The generated InitializeMonitorMap registered the PModule coverage metadata AFTER runtime.RegisterMonitor<...>(), but the monitor's start-state entry is logged DURING RegisterMonitor, so it couldn't be classified. Fixes: - Observer: replace the ctor snapshot with a live Refresh() that re-reads PModule whenever coverageMonitors has grown (called from OnMonitorStateTransition and the accessors), so the first iteration and any late-registered monitor are picked up. - Codegen: emit PModule.coverageMonitors.Add / scenarioStateCounts BEFORE RegisterMonitor so the start-state entry is classifiable. Verified end-to-end: a `p check -s 1` run now reports scenario coverage and writes the *_scenario_coverage.json artifact (both previously missing), and partial progress now includes the start state (e.g. an unsatisfiable scenario reports 2/4 states on -s 1). Full Release suite green (759). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
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.
Summary
This PR brings the Fest (NSDI'26) design-testing capabilities to PChecker and adds
tooling + an empirical evaluation around them. It has grown into a coherent, dependent
stack; everything is flag-gated with the historical behavior as the default, so
p checkwith no new flags is unchanged.Five feature areas + an evaluation:
1. Scenario coverage (RQ3 of the paper)
scenario Name observes {..} { ..states.. }construct that lowersto a P spec monitor with a coverage flag: auto-attached to every test case (no
assertneeded), its accepting (cold) state means "this behavior was exercised",and it is exempt from the liveness check (an unsatisfied scenario is uncovered,
not a bug). Compile-time warning if a
scenariohas no cold state.partial coverage (best
X/Ystates for scenarios never satisfied). The report wasredesigned for understandability — a summary count, covered-vs-gap grouping, and
gaps called out explicitly.
p merge-scenario-coverage [dir]aggregates per-run*_scenario_coverage.jsonartifacts into one suite-wide report, listing which test cases cover each scenario.
2. Feedback-search fidelity (Cluster B)
1 − Jaccard, decoupled from the mutation budget), instance-granular abstract Lamport timelines (
id.Name), and ~5-int mutation.3. Coverage-novelty scenario steering (D4)
scenariocompliance now feeds the feedback search as a sparse coverage-noveltysignal (reward first-satisfaction / new furthest state), replacing a signal that
saturated at 1.0 and was a no-op. Computed only for kept generators (after the diversity
gate). Also fixed
VectorTime.CompareToto compare the union of both clocks' keys.4. Pluggable timeline representations (
--timeline-repr)with today), kgram (higher-resolution local order), causal (cross-machine
happens-before, reusing the runtime's already-computed vector clocks), hybrid.
Plus
--timeline-payload.TimelineObserverkeeps the shared MinHash/gate; only thetoken content changes.
5. Robust per-test-case output layout
PCheckerOutput/<testCase>/<Mode>/—with history rotation scoped per test case (previously a single shared
<Mode>/dirwas rotated per invocation). This fixes test cases clobbering each other's history and a
Directory.Moverace between concurrent runs of different test cases; andp merge-scenario-coveragenow keeps only the latest artifact per test case, sore-runs / rotated-history copies never double-count. A single anonymous run (no
-tc)keeps the old layout. Behaviour change: default output paths now include the
<testCase>segment — anything scriptingPCheckerOutput/BugFinding/…should update.(PEx/symbolic
--outdiris unchanged.)Evaluation (honest, independently audited)
An extensive empirical study lives in
eval/fest-scenario-coverage/(report +example scenarios). Headline findings, stated plainly:
--sch-randomis the most effective bug-finder — itbeats every feedback variant (all timeline representations) on all bugs (safety 4–5×
faster; the one liveness bug fastest + 100% found). Feedback's exploitation appears to
hurt at this scale.
liveness bug
causalis the strongest feedback repr (significantly >kgram) andkgramthe weakest; for safety bugs it is immaterial.causalworst on smallrequest/response models, best on larger/concurrent ones;
kgram/hybridthe reverse).--timeline-payload(whole-payload hashing) is too fine and degenerates — it needsselective-field hashing.
censoring, modest seed counts. Results are directional. The open question is whether
feedback (and a richer representation) pays off on production-scale state spaces.
Because of this, all new search behavior is opt-in and the default stays
pairwise/non-feedback — no default flip is proposed here.
Verification
timeline representations, and the per-test-case output layout + latest-only merge
(
Tst/UnitTests/{ScenarioCoverageTest,TimelineRepresentationTest}.cs).--timeline-repr pairwiseverifiedbyte-identical to the default; same-
--seedruns reproducible; per-test-case output +dedupe verified end-to-end (a re-run rotates only its own folder and is merged once).
the old output path.
Notes / follow-ups
--timeline-payload: selective-field hashing.in the stack.
🤖 Generated with Claude Code