Fest scenario coverage: robustness hardening (cold start-state, merge version guard, dead liveness overload)

[ankushdesai]

End-to-end robustness pass over the Fest scenario-coverage feature (follow-up to #985). An adversarial audit across six dimensions (compiler/codegen, satisfaction detection, liveness exemption, report/merge/artifact, output-layout/CLI, feedback-steering) surfaced one real correctness bug and two hygiene/robustness gaps. All fixed here; verified end-to-end; full Release suite green (762/762).

Fixes

1. A cold start state was trivially "covered" (correctness).
A scenario whose start state is cold was marked satisfied on its RegisterMonitor start-entry — before any behavior was observed — so it reported [covered] in every schedule (a coverage measurement that lies). Satisfaction now ignores the monitor's first (start) state entry via a small pure predicate ScenarioSteering.IsSatisfyingEntry(isInHotState, isStartEntry), so such a scenario is a gap until observed behavior re-enters a cold state. The compiler also now warns on a cold start state. Normal start hot state ... cold state Done scenarios are unaffected.

Empirically confirmed: a probe scenario observing a never-sent event flipped from [covered] triggered in 5 schedules → [GAP]; the example ClientServer scenarios still report 4/5 covered.

2. merge-scenario-coverage ignored its own schema Version (robustness).
MergeDirectory deserialized every artifact as v1 regardless of version, so a future-schema artifact would be silently miscounted. It now skips newer-version artifacts loudly — which is what the Version field was written for.

3. Dead CheckLivenessTemperature(int) overload (hygiene).
Unlike the live parameterless method, it lacked the coverage-monitor liveness exemption — a latent footgun if ever wired up. Removed.

Tests

• IsSatisfyingEntry_ColdStateSatisfies_ExceptTheStartEntry — locks the cold-start semantics.
• MergeDirectory_SkipsArtifactsFromANewerSchemaVersion — a version: 999 artifact is skipped, not counted.
• Full Release UnitTests suite: 762/762 (was 760; +2).

Considered and not changed

• Rejected a "floating-point priority non-determinism" flag: it's a List linear-scan insertion (not unordered iteration); same-seed runs produce bit-identical doubles → deterministic order.
• Deferred as low-risk / not reachable in the current architecture: a theoretical race on PModule static maps (PChecker parallelism is process-based), Count-only change detection, the mtime tie-break in merge dedupe, and summed-vs-unioned distinct-timeline counts across test cases.

🤖 Generated with Claude Code

[Copilot]

Pull request overview

Hardens the Fest scenario-coverage pipeline end-to-end by fixing a correctness hole in scenario satisfaction (cold start state being counted as “covered” before any observed behavior), adding a forward-compatibility guard to the merge tool, and removing a dead/unsafe liveness-check overload.

Changes:

• Prevent scenarios from being marked satisfied on the monitor’s initial (start) cold-state entry by introducing ScenarioSteering.IsSatisfyingEntry(isInHotState, isStartEntry) and wiring it into scenario satisfaction detection.
• Add a schema-version guard in merge-scenario-coverage to loudly skip artifacts with a newer Version than the tool supports.
• Remove the unused Monitor.CheckLivenessTemperature(int) overload and add unit coverage for the new semantics + version-skipping behavior.

Reviewed changes

Copilot reviewed 5 out of 7 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
Tst/UnitTests/ScenarioCoverageTest.cs	Adds unit tests for cold-start satisfaction semantics and skipping newer-schema artifacts during merge.
Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs	Adds a compiler warning when a scenario’s start state is marked cold (accepting).
Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/ScenarioSteering.cs	Introduces the centralized predicate defining when a state entry should satisfy a scenario.
Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/ScenarioComplianceObserver.cs	Tracks and excludes the monitor’s first (start) state entry from satisfaction detection.
Src/PChecker/CheckerCore/SystematicTesting/ScenarioCoverageMerger.cs	Skips artifacts whose schema Version is newer than SchemaVersion to avoid silent miscounts.
Src/PChecker/CheckerCore/Runtime/Specifications/Monitor.cs	Removes the dead CheckLivenessTemperature(int) overload.
eval/fest-scenario-coverage/README.md	Documents the “observed behavior required” rule and the cold-start warning guidance.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[ankushdesai]

Summary — scenario-coverage robustness + soundness/completeness verification

This PR hardens the Fest scenario-coverage feature, verifies it is sound, closes the test gaps around its high-risk seams, and fixes a pre-existing compiler concurrency bug found along the way. Full Release suite green: 774/774. Three commits:

1. Robustness fixes (bd75ffee3)

• Cold start state no longer trivially "covered" — a scenario whose start state is cold was marked satisfied on its RegisterMonitor start-entry (before any behavior), so it reported [covered] in every schedule. Satisfaction now ignores the monitor's first (start) entry (ScenarioSteering.IsSatisfyingEntry); the compiler also warns on a cold start state. Normal hot→cold scenarios unaffected.
• merge-scenario-coverage honors the artifact schema Version — a newer-schema artifact is skipped loudly instead of silently miscounted as v1.
• Removed the dead CheckLivenessTemperature(int) overload that lacked the coverage-monitor exemption (latent footgun).

2. Automated tests for the high-risk seams (7f87f4787)

Previously only leaf/pure logic was tested. Added: cold-start fix end-to-end at the observer; the Refresh lazy-init (-s 1 silent-drop hazard); merge/report graceful-degradation (corrupt JSON, empty dir) and zero-scenario contracts. ([InternalsVisibleTo(UnitTests)] added to PCheckerCore so the internal observer is testable.)

3. Compiler parallel-compile race fix + suite completion (463f89993)

While adding tests, parallel in-process compilation intermittently crashed with "Operations that change non-concurrent collections must have exclusive access … corrupted its state." A whole-compiler audit found 5 static mutable fields shared across concurrent compiles (each backend codegen is a singleton, so [ThreadStatic] is the right isolation; every field is written before read within a compile):

• InferMachineCreates._visitedFunctions (the crash cause; always-run type-check path)
• PEx PExCodeGenerator._globalParams, TransformASTPass.{context,continuationNumber,callNum}
• PVerifier Uclid5CodeGenerator.useLocalPrefix (+ per-compile reset)
• PObserve Constants._reservedWords → Lazy<T>

Plus the remaining tests: liveness-exemption non-leak guard (codegen test: a real spec is not added to coverageMonitors while the scenario is, metadata before RegisterMonitor), FeedbackGuidedStrategy integration (diversity-gate-before-novelty ordering; per-instance suite state), MachineChecker warnings, and same-seed determinism. Also relabeled the merged report's cross-test-case count to "satisfying timelines (summed per test case)" (it is a per-test-case sum, not global-distinct).

Verification

Soundness was checked by an adversarial review pass with falsification probes (no false-covered, no false liveness bugs, no crashes, deterministic). Notably, the liveness-exemption non-leak was empirically bisected — a real spec + a coexisting scenario behaves identically to a bare spec, i.e. the scenario does not suppress real liveness enforcement — and is now guarded by the codegen test above.

🤖 Generated with Claude Code