add specification testing

[AnthonyLloyd]

No description provided.

[Copilot]

🟡 Changes recommended

The TerminationDetection specification’s boundary predicate contradicts its own “unbounded above and below”/“verbatim StateConstraint” claim by only bounding upper ranges, which likely impacts the modeled state space and published-number comparisons.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

This PR introduces and documents Spec-based specification testing in CsCheck (exhaustive state-space exploration plus temporal/trace-style requirements), alongside a substantial set of worked examples and scale/robustness tests that demonstrate and validate the feature set.

Changes:

• Added multiple specification-testing worked examples (FIX session core, refresh-on-access cache, fencing tokens, blocking queue, alternating bit protocol, disruptor, and Safra termination detection).
• Added documentation for Spec (usage guide + design rationale) and updated README/LLM guidance to include specification testing and operation coverage/classify output.
• Updated package metadata (tags/version/release notes) and solution/docs wiring to surface the new materials.

File summaries

File	Description
Tests/Specs/TerminationDetectionTests.cs	Adds tests validating the Safra/EWD998 specification behavior and recorded comparisons vs published TLC figures.
Tests/Specs/TerminationDetectionSpec.cs	Adds the Safra/EWD998 executable specification, requirements, and boundary constraint.
Tests/Specs/SpecScaleTests.cs	Adds performance/scale and determinism tests for Spec.Exhaustive across sizes and thread counts.
Tests/Specs/SpecIntroTests.cs	Adds an introductory, small-state example that demonstrates the Spec workflow end-to-end.
Tests/Specs/RefreshCacheTests.cs	Adds proof/sample/faults/conformance tests for the refresh-on-access cache example.
Tests/Specs/RefreshCacheSpec.cs	Adds the refresh-on-access cache specification with invariants/rules/faults demonstrating interleaving.
Tests/Specs/RefreshCache.cs	Adds an imperative cache implementation used for Conform testing against the spec.
Tests/Specs/FixEngineTests.cs	Adds proof/sample/faults/conformance tests for the FIX session-core specification.
Tests/Specs/FixEngineSpec.cs	Adds the FIX 4.4 session-core executable specification and its requirements/fault suite.
Tests/Specs/FixEngine.cs	Adds an imperative session-engine implementation used for Conform testing (with a planted defect).
Tests/Specs/FencingTests.cs	Adds tests comparing three fencing-token configurations to select a safe design.
Tests/Specs/FencingSpec.cs	Adds the fencing-token specification with requirements/faults across configurations.
Tests/Specs/DisruptorTests.cs	Adds boundary-focused disruptor invariant tests, including “raise the boundary” checks and fault testing.
Tests/Specs/DisruptorSpec.cs	Adds the disruptor specification with a Boundary for inherently infinite state space.
Tests/Specs/BlockingQueueTests.cs	Adds tests demonstrating deadlock, fixes, oracle agreement, and published-closed-form agreement.
Tests/Specs/BlockingQueueSpec.cs	Adds the blocking-queue specification with parameterized wake strategies and supporting helpers.
Tests/Specs/AlternatingBitTests.cs	Adds tests checking textbook predictions and requirement strength via faults.
Tests/Specs/AlternatingBitSpec.cs	Adds the alternating-bit protocol specification (including AtMost usage) plus reachability guards.
Tests/CheckTests.cs	Adds tests for model-based classify/operation coverage output and failure-survival behavior.
README.md	Updates the main docs to include specification testing and operation coverage, and reorganizes sections.
llms.txt	Updates “assistant-facing” guidance to include Spec and classify/coverage notes and correct doc links.
docs/SpecDesign.md	Adds a design record explaining the Spec feature’s shape, tradeoffs, and lessons from examples.
docs/Spec.md	Adds the main Spec user guide describing requirement forms, proof model, faults, boundary, and patterns.
docs/GettingStarted.md	Adds a “Specification testing” primer section pointing readers to the new Spec materials.
CsCheck/CsCheck.csproj	Updates package description/tags/version and release notes to include Spec and related features.
CsCheck.slnx	Adds new Spec docs to the solution file list so they show up in solution view.
AGENTS.md	Adds contributor guidance/examples for Spec and classify/coverage output in model-based testing.
.gitattributes	Adds *.slnx EOL configuration.

Review details

• Files reviewed: 31/31 changed files
• Comments generated: 1
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

🟢 Approval recommended

The changes are largely additive (new specs/tests/docs) with only a minor doc-comment formatting nit to consider.

Review details

• Files reviewed: 33/33 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🔵 Needs a closer look

TerminationDetectionTests appears likely to add significant CI runtime/memory load (multiple large Exhaustive/Faults runs) and should be tightened or gated to avoid destabilizing/slow CI.

Review details

Suppressed comments (3)

Previously missed (3) — in code that hasn't changed since the last review.

Tests/Specs/TerminationDetectionTests.cs:85

• Growth_With_The_Bound runs 4 full Exhaustive explorations (including the 1.5M-state original bound). This is likely to add noticeable runtime and memory pressure to CI despite being primarily diagnostic output. Consider marking this as long-running (consistent with other tests in the repo) or reducing it to a smaller bound / fewer rows.
  Tests/Specs/TerminationDetectionTests.cs:103
• Dropping_Rule_3_Detects_Termination_Early currently only asserts the fault is caught by something (Uncaught empty) and prints the catcher. To make this a stable regression test (and to ensure it actually demonstrates the stated safety property), assert which requirement catches NoBlackenOnReceive (e.g., TERMINATION-DETECTION, if that's the intended one).
  Tests/Specs/TerminationDetectionTests.cs:70
• In The_Interesting_States_Are_All_Reached, report.ToString() is recomputed on every loop iteration. Since the report string can be large, compute it once and reuse it for the Contains checks.

• Files reviewed: 33/33 changed files
• Comments generated: 0 new
• Review effort level: Lite

[Copilot]

🔵 Needs a closer look

It introduces a large new verification/testing surface area with many new example specs and docs, and warrants final human review for completeness and long-term maintenance impact.

Review details

Suppressed comments (1)

Previously missed (1) — in code that hasn't changed since the last review.

Tests/PcgThreadAffinityTests.cs:20

• The XML doc comment closes the mid-sentence, leaving the rest of the sentence outside the paragraph; this renders oddly in generated docs and is easy to fix by moving the closing tag to the end of the sentence.

• Files reviewed: 32/33 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🔵 Needs a closer look

TerminationDetectionSpec doesn’t mark detected states as Terminal, so Exhaustive will report intended completion states as deadlocks, reducing the signal of DeadlockStates/DeadlockTrace for real modeling errors.

Review details

Suppressed comments (1)

Previously missed (1) — in code that hasn't changed since the last review.

Tests/Specs/TerminationDetectionSpec.cs:103

• Detected states appear to be intended end states, but the spec does not mark them as Terminal. In a detected state (Pos==0, white token, C0+Q==0, node 0 white + inactive), none of the declared actions are enabled, so Exhaustive will report these as deadlocks, which makes DeadlockStates/DeadlockTrace less meaningful for spotting real modelling dead-ends. Consider declaring detected states as terminal so a closed proof doesn’t look like a deadlocking protocol.

• Files reviewed: 33/34 changed files
• Comments generated: 0 new
• Review effort level: Lite

[Copilot]

🟡 Changes recommended

One of the new “proof” tests uses a broad transition-count range where the closed exhaustive model should allow pinning an exact deterministic count, weakening regression detection.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Review details

• Files reviewed: 33/34 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🟢 Approval recommended

The only feedback is a minor maintainability tweak (making an invisible NBSP explicit) and no functional/test correctness issues were found.

Review details

Suppressed comments (1)

Previously missed (1) — in code that hasn't changed since the last review.

Tests/CheckTests.cs:281

• Leaf embeds a literal U+00A0 non‑breaking space, which is visually indistinguishable from a normal space and easy to break accidentally in edits/copy-paste. Using an explicit escape keeps the intent clear while preserving the test behavior.

• Files reviewed: 33/34 changed files
• Comments generated: 0 new
• Review effort level: Lite

[Copilot]

🟢 Approval recommended

The changes are cohesive (docs + examples + targeted library/support updates), and no correctness or build-breaking issues were identified in the reviewed diffs.

Review details

• Files reviewed: 33/34 changed files
• Comments generated: 0 new
• Review effort level: Lite