Add exploration verdict, strict mode and machine-readable JSON report

[Chao-Shiun]

Summary

Today coyote test exits with code 0 whenever no bug was found, even when the exploration was not exhaustive: the test invoked APIs that Coyote does not control (partially controlled concurrency is allowed by default), iterations were truncated by the --max-steps bound, or the test contains no scheduling decisions at all. A human can spot these conditions in the text report, but scripts and automated agents that drive the tester only see the exit code and have to parse the .txt output.

This PR makes the outcome of an exploration machine-readable. Everything is opt-in; exit codes and emitted files are unchanged unless the new options are used.

Exploration verdict

• TestReport.GetVerdict() returns an ExplorationVerdict with a Status (Complete, Incomplete, BugFound, InternalError), the Reasons that make the exploration incomplete (UncontrolledInvocations, TruncatedExecutionPaths, ExceededUnfairStepsBound, InsufficientExecutionPaths, NoSchedulingDecisions) and Warnings.
• TestReport.NumOfTruncatedPaths exposes the number of execution paths that were cut by the max-steps bound (MaxFairStepsHitInFairTests + MaxUnfairStepsHitInUnfairTests).
• The verdict is printed in the text report as Exploration verdict: ....

Fair execution paths that exceed the unfair max-steps bound (already counted in MaxUnfairStepsHitInFairTests) terminate normally after switching to fair scheduling, so they are reported as a warning rather than as truncation.

Strict mode

• Configuration.WithStrictExplorationEnabled() / --strict: when no bug was found but the verdict is Incomplete, the tool exits with the new code 4 (IncompleteExploration). A found bug still exits with 2.
• Configuration.WithStrictBoundCheckingEnabled() / --strict-bounds: additionally treats fair execution paths that exceeded the unfair max-steps bound as incomplete exploration.

JSON report

• Configuration.WithJsonReportEnabled() / --json-report emits <name>.report.json next to the other reports. It contains the verdict, the exploration statistics, the bug reports, the uncontrolled invocations, the settings used during testing, the identity of the tested assembly (path, SHA-256, whether it was rewritten) and the paths of the other emitted reports, such as the reproducible .trace file.
• TestingEngine.GetJsonReport() returns the same document in-process.

Abbreviated example for a run with an uncontrolled Task.ContinueWith:

{
  "coyoteVersion": "1.7.11.0",
  "testName": "CliE2E.Scenarios.UncontrolledTest",
  "assembly": { "name": "Harness", "path": "...", "sha256": "14AFA0DE...", "isRewritten": true },
  "settings": { "strategy": "portfolio[fair,seed:...]", "iterations": 5, "isStrictExplorationEnabled": true, "...": "..." },
  "verdict": { "status": "Incomplete", "reasons": ["UncontrolledInvocations", "NoSchedulingDecisions"], "warnings": [] },
  "bugs": { "count": 0, "reports": [] },
  "uncontrolledInvocations": ["System.Threading.Tasks.Task.ContinueWith"],
  "exploration": { "fairPaths": 5, "unfairPaths": 0, "uniquePaths": 1, "truncatedFairPaths": 0, "...": "..." },
  "artifacts": { "uncontrolledInvocations": "...\\Harness_0.uncontrolled.json" },
  "elapsedSeconds": 0.14
}

Related: #261 asked for a way to know whether a test ended because of uncontrolled concurrency; the verdict reasons and the uncontrolledInvocations array cover that case.

Compatibility

• Default exit codes are unchanged (0, 2, 3); 4 is only returned with --strict or --strict-bounds.
• No existing TestReport member changed; the new members are additive and the verdict is derived, so Merge and Clone are unaffected.
• The only change visible without the new options is the additional Exploration verdict: line in the text report (and an Exploration warnings: line when applicable). The TestingEngineLoggingTests expectations were updated accordingly.

Testing

• New tests in Tests/Tests.BugFinding/Reports: verdict statuses and reasons (complete, uncontrolled invocation, truncated paths, no scheduling decisions, bug found), warning vs. strict bound checking for paths exceeding the unfair bound, and the JSON report contents both in-process and as an emitted file with artifact paths.
• Tests.BugFinding (701), Tests.Runtime (54), Tests.Actors.BugFinding (361) and Tests.Tools (2) pass on net8.0.
• End-to-end with the coyote CLI on a small rewritten assembly: exit code 0 (complete), 0 (uncontrolled invocation without --strict), 4 (uncontrolled invocation with --strict), 2 (bug), and the .report.json contents shown above.
• Reference docs were regenerated with the GenDoc + InheritDocTool pipeline from Scripts/gen-docs.ps1; unrelated generator drift was left out of this change.

[Chao-Shiun]

@microsoft-github-policy-service agree