CsCheck Random Testing Library

CsCheck is a random testing library for C# that provides a more automated and powerful alternative to traditional example-based testing. Instead of manually writing a few test cases, you define generators that allow the library to run hundreds or thousands of examples with varying sizes and edge cases (e.g., empty collections, values summing to zero).

Key benefits include:

• Automated Edge Case Discovery: Finds quirky or large examples that developers might overlook.
• Parallel Execution: Tests run in parallel by default, allowing millions of examples to be processed in a short timeframe (e.g., 60 seconds).
• Shrinking: When a bug is found, CsCheck automatically shrinks the failing input to the smallest possible example, making reproduction and diagnosis significantly easier.
• Stronger Guarantees: A test that runs a vast number of generated examples provides a much stronger claim of correctness than a handful of manual examples.

CsCheck's Spec testing is designed to address a gap in existing property-based testing (PBT) tools. While most PBT libraries (like Hypothesis, ScalaCheck, or FsCheck) focus on checking properties one transition at a time (per-command postconditions), CsCheck allows for specifications that are not tied to a single transition.

Key differentiators include:

• Soundness on Cycles: Unlike some model checkers where 'eventually' properties might fail on cycles, CsCheck incorporates obligations (like response deadlines) into the search state. This ensures that cycles carrying unmet obligations are correctly reported.
• Unified Specification: A single specification object is shared between the exhaustive engine and the shrinking random engine.
• Vacuity Detection: CsCheck identifies and reports when a requirement passes simply because its antecedent (the condition required to trigger the check) never occurred. This is presented as a default feature in every run.
• State-Space Reduction: Symmetry reduction is achieved by defining a custom Equals implementation for your state type S, effectively treating symmetry as a coarser equality.

The performance and memory consumption of a specification are primarily determined by the state S.

Memory Constraints:

• The binding constraint is memory, not CPU.
• The default maxStates is 10,000,000, which consumes approximately 2GB to 3GB of RAM depending on the state width.
• Memory usage is roughly 170-305 bytes per state.

Performance Optimization (Keep S narrow):

• Width in bytes: Every guard, transition, and requirement predicate receives S by value. A wide state (many unused fields) increases the cost of every single operation due to copying.
• Distinct values: A state with many distinct values (wide state space) makes it harder for the engine to close the space.
• Optimization Tip: If a model is slow, check for unused fields. Packing small fields into a single int (e.g., using bits for booleans) can significantly improve ns/transition speed.

CsCheck uses the Spec abstraction to define the intended behavior of a stateful system. Once a specification is written, you can verify it using four distinct testing modes, each offering different guarantees and costs:

1. Exhaustive: Enumerates the entire reachable state space. If the state space closes, your requirements are mathematically proved for the model. This is very fast for protocol state machines.
2. Sample: Performs random walks through the state space with CsCheck shrinking. This is used for models too large to be exhausted, using a standard iter/time budget.
3. Faults: Injects declared defects into the model and reports which requirement catches them. This acts as mutation testing for your specification to ensure your requirements are actually meaningful and capable of catching errors.
4. Conform: Drives a real-world implementation through the same state walks generated by the spec to ensure the actual code conforms to the specification.

Recommended Workflow: Start with Exhaustive to prove the model, but prioritize Faults next. Faults ensures your requirements aren't passing 'for the wrong reason' or passing vacuously (e.g., a requirement that can never fail).

/* The relationship between testing modes: */
// spec -> Exhaustive -> (if closed) -> Faults -> Conform
// spec -> Exhaustive -> (if not closed) -> Boundary -> Exhaustive
// spec -> Exhaustive -> (if not closed) -> Sample -> SampleFaults -> Conform

When running Spec.Exhaustive, the engine performs a breadth-first walk of the reachable state space. A CLOSED state space indicates a formal proof for the abstracted model, meaning every reachable state has been visited and no violations were found.

Key Metrics in the Report

• Triggered: The number of times a requirement's condition was met.
  • Crucial Note: If a requirement shows NEVER or a low number, it may mean the 'when' or 'on' trigger was never actually exercised, meaning the requirement hasn't actually been tested.
  • Invariants and Rules without specific triggers apply to every step.
• Unresolved (Sample mode only): Response obligations that were still outstanding when the trace ended. This does not indicate a failure, but suggests traces should be run longer.
• deadlock: The number of states with no enabled actions that were not explicitly declared Terminal. In a protocol model, this should ideally be zero. If non-zero, use report.DeadlockTrace to find the path to the dead end.
• Fired: The count for each (action, argument) case. This is more granular than counting per action. A NEVER here means a specific argument case (e.g., a specific error code in a Recv action) never ran.

Interpreting Counterexamples

If the search does not close, the engine provides the shortest path to the violation due to the breadth-first search approach. The trace will show the sequence of actions and the state of requirements (e.g., exp for expected, out for outstanding) leading to the failure.

Specification testing allows you to define requirements for a state machine (a protocol, rules, or regulations) and verify them. You define a specification using Spec.From(initialState) and then chain several types of definitions:

• Action: Defines a transition. Includes a predicate for when the action is valid, the transition logic, and an optional weight for sampling.
• Rule: Defines a requirement that must hold. Uses when (the condition) and then (the expected outcome).
• Response: Defines a temporal requirement. It specifies a trigger condition and a response that must occur within a certain interval, checked per a specific action (e.g., per: "Tick").
• Never: Defines a negative requirement (e.g., "this should never happen").
• Reachable: Defines a goal state that must be reachable from the initial state.

Once defined, you can run the specification using different modes:

• Exhaustive: Proves the requirements for the entire reachable state space (breadth-first).
• Sample: Performs random walks for large models.
• Faults: Injects defects to see if your requirements actually catch them (mutation testing for specs).
• Conform: Drives a real implementation through the same traces used by the specification to ensure the implementation matches the model.

Spec.From(State.Connected)
.Action("Recv", Inbound, (s, _) => s.Status != Disconnected, (s, m) => s.Inbound(m), weight: 30)
.Action("Tick", s => s.Status != Disconnected, s => s.Tick(), weight: 20)
.Rule("SEQ-TOO-LOW-FATAL",
    "MsgSeqNum lower than expected without PossDupFlag set to Y is a fatal error: send a Logout and terminate.",
    when: (b, a) => b.Up && a.RecvSeq == Seq.TooLow,
    then: (b, a) => a.Put(Out.Logout) && a.Status == Disconnected)
.Response("LOGOUT-COMPLETES",
    "The initiator of a Logout waits for the confirming Logout, and terminates anyway if it does not arrive.",
    trigger:  (b, a) => a.Status == LogoutSent && b.Status != LogoutSent,
    response: (b, a) => a.Status == Disconnected,
    within: Interval + 1, per: "Tick")
.Never("DISCONNECTED-SILENT", "No message is sent on a terminated connection.",
    (b, a) => b.Status == Disconnected && a.Sent != Out.None)
.Reachable("CAN-LOG-ON", "A session can reach the logged on state at all.",
    s => s.Status == LoggedOn);

The Exhaustive engine determines if it has found a new state by checking equality. You can override Equals and GetHashCode to control what constitutes a distinct state.

Symmetry Reduction

You can implement symmetry reduction by canonicalizing interchangeable subjects within your Equals and GetHashCode methods. This collapses multiple states into one, saving significant computation time.

Warning:

1. Soundness: If you use symmetry reduction, your requirements must also be symmetric. If a requirement names a specific subject (e.g., "Client One is never refused"), collapsing Client One and Client Two into one state will hide failures, making the proof silently false.
2. Precision: An Equals implementation that is too coarse will merge genuinely different states, leading to false proofs. An implementation that is too fine will simply increase the state space and slow down the search.

// Example of symmetry reduction: Two clients that differ only in which is which are treated as one state.
public bool Equals(State other)
    => Holder == other.Holder && Fenced == other.Fenced
    && (One.Equals(other.One) && Two.Equals(other.Two)
     || One.Equals(other.Two) && Two.Equals(other.One));