agenticraft_foundation.verification.counterexamples

Structured counterexample generation for refinement and equivalence failures.

Given a raw counterexample trace from refinement or equivalence checking, this module walks through both LTS step-by-step, identifies the exact divergence point, and produces human-readable explanations.

Structured counterexample generation for refinement and equivalence failures.

This module provides: - Annotated trace explanations showing exactly where and why verification fails - Divergence point identification in refinement failures - Distinguishing event analysis for equivalence failures

Theory: Synchronized product of spec/impl LTS + BFS divergence search (Roscoe, 1994 - Theory and Practice of Concurrency).

Given a refinement or equivalence failure with a raw counterexample trace, this module walks the trace through both LTS step-by-step, recording what each side can do at each point, and identifies the exact divergence.

StepStatus

Bases: Enum

Status of a single step in an annotated trace.

AnnotatedStep dataclass

A single step in an annotated trace.

ATTRIBUTE	DESCRIPTION
event	The event performed at this step. TYPE: Event
status	Whether this step was OK or a VIOLATION. TYPE: StepStatus
spec_available	Events available in the spec LTS at this point. TYPE: frozenset[Event]
impl_available	Events available in the impl LTS at this point. TYPE: frozenset[Event]
spec_states	Set of spec state IDs after tau-closure at this point. TYPE: frozenset[int]
impl_states	Set of impl state IDs after tau-closure at this point. TYPE: frozenset[int]

CounterexampleExplanation dataclass

Structured explanation of why a verification check failed.

Provides a human-readable summary, an annotated trace showing each step's status, and the precise divergence point where spec and impl disagree.

ATTRIBUTE	DESCRIPTION
summary	Human-readable summary of the failure. TYPE: str
annotated_trace	List of annotated steps showing the trace walkthrough. TYPE: list[AnnotatedStep]
divergence_point	Index in the trace where divergence occurs, or -1 if the trace itself is the issue (e.g., empty trace divergence). TYPE: int
spec_allowed	Events the spec allows at the divergence point. TYPE: frozenset[Event]
impl_attempted	The event the impl attempted (or None for refusal issues). TYPE: Event | None
failure_kind	The kind of failure ("trace", "failures", "equivalence"). TYPE: str
raw_counterexample	The original raw counterexample from the checker. TYPE: Trace | Failure | None

explain_refinement_failure(spec, impl, result)

Generate a structured explanation for a refinement failure.

Takes the raw counterexample from a refinement check and walks it through both spec and impl LTS, identifying the exact divergence point.

PARAMETER	DESCRIPTION
spec	The specification process or LTS. TYPE: Process | LTS
impl	The implementation process or LTS. TYPE: Process | LTS
result	The RefinementResult containing the raw counterexample. TYPE: RefinementResult

RETURNS	DESCRIPTION
CounterexampleExplanation	CounterexampleExplanation with annotated trace and divergence details.

RAISES	DESCRIPTION
ValueError	If result indicates refinement holds (no failure to explain).

explain_equivalence_failure(p, q, result)

Generate a structured explanation for an equivalence failure.

Takes the raw witness trace from an equivalence check and walks it through both LTS, identifying where the two processes first disagree.

PARAMETER	DESCRIPTION
p	The first process or LTS. TYPE: Process | LTS
q	The second process or LTS. TYPE: Process | LTS
result	The EquivalenceResult containing the raw witness. TYPE: EquivalenceResult

RETURNS	DESCRIPTION
CounterexampleExplanation	CounterexampleExplanation with annotated trace and divergence details.

RAISES	DESCRIPTION
ValueError	If result indicates equivalence holds (no failure to explain).

find_minimal_counterexample(spec, impl, max_trace_length=50)

Find the shortest counterexample trace and explain it.

Performs a BFS over the synchronized product of spec and impl LTS to find the shortest trace where they diverge.

PARAMETER	DESCRIPTION
spec	The specification process or LTS. TYPE: Process | LTS
impl	The implementation process or LTS. TYPE: Process | LTS
max_trace_length	Maximum trace length to search. TYPE: int DEFAULT: 50

RETURNS	DESCRIPTION
CounterexampleExplanation | None	CounterexampleExplanation for the shortest diverging trace,
CounterexampleExplanation | None	or None if impl refines spec up to max_trace_length.