agenticraft_foundation.algebra.refinement

Refinement checking — trace refinement, failures refinement, and failures-divergence refinement.

Refinement checking for CSP processes.

This module provides: - Trace refinement: SPEC ⊑_T IMPL iff traces(IMPL) ⊆ traces(SPEC) - Failures refinement: SPEC ⊑_F IMPL iff failures(IMPL) ⊆ failures(SPEC) - Failures-divergences refinement (FD): Standard CSP refinement

Refinement is the key relation for verification: - SPEC describes allowed behaviors - IMPL must not have behaviors outside SPEC - If IMPL ⊑ SPEC, IMPL is a valid implementation

Note on direction: - In CSP: SPEC ⊑_T IMPL reads "SPEC is trace-refined by IMPL" - This means traces(IMPL) ⊆ traces(SPEC): IMPL has fewer behaviors - Equivalently: IMPL does nothing outside what SPEC allows

RefinementResult dataclass

Result of a refinement check.

is_valid property

True if implementation refines specification.

RefinementReport dataclass

Detailed refinement analysis report.

overall_result property

True if all refinement checks pass.

DivergenceResult dataclass

Result of divergence check.

trace_refines(spec, impl, max_trace_length=100)

Check trace refinement: traces(IMPL) ⊆ traces(SPEC).

An implementation trace-refines a specification if every trace of the implementation is also a trace of the specification.

PARAMETER	DESCRIPTION
spec	The specification process TYPE: Process | LTS
impl	The implementation process TYPE: Process | LTS
max_trace_length	Maximum trace length to check TYPE: int DEFAULT: 100

RETURNS	DESCRIPTION
RefinementResult	RefinementResult with counterexample if refinement fails

failures_refines(spec, impl, max_trace_length=50)

Check failures refinement: failures(IMPL) ⊆ failures(SPEC).

An implementation failures-refines a specification if every failure of the implementation is also a failure of the specification.

This is stronger than trace refinement: not only must traces match, but refusal sets must also be subsets.

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

RETURNS	DESCRIPTION
RefinementResult	RefinementResult with counterexample if refinement fails

check_divergence_free(process, max_depth=1000)

Check if process is divergence-free.

A process diverges if it can perform an infinite sequence of τ actions. This is detected by finding τ-cycles in the LTS.

PARAMETER	DESCRIPTION
process	The process to check TYPE: Process | LTS
max_depth	Maximum exploration depth TYPE: int DEFAULT: 1000

RETURNS	DESCRIPTION
DivergenceResult	DivergenceResult indicating divergence-freedom

fd_refines(spec, impl, max_trace_length=50)

Check failures-divergences refinement.

This is the standard CSP refinement: IMPL ⊑_FD SPEC iff: 1. failures(IMPL) ⊆ failures(SPEC) 2. divergences(IMPL) ⊆ divergences(SPEC)

If SPEC is divergence-free, then IMPL must also be divergence-free.

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

RETURNS	DESCRIPTION
RefinementResult	RefinementResult

analyze_refinement(spec, impl, spec_name='SPEC', impl_name='IMPL', max_trace_length=50, check_failures=True)

Perform comprehensive refinement analysis.

PARAMETER	DESCRIPTION
spec	The specification process TYPE: Process
impl	The implementation process TYPE: Process
spec_name	Name for the spec in reports TYPE: str DEFAULT: 'SPEC'
impl_name	Name for the impl in reports TYPE: str DEFAULT: 'IMPL'
max_trace_length	Maximum trace length TYPE: int DEFAULT: 50
check_failures	Whether to check failures refinement TYPE: bool DEFAULT: True

RETURNS	DESCRIPTION
RefinementReport	RefinementReport with detailed analysis

refines(spec, impl, mode='trace')

Check if implementation refines specification.

PARAMETER	DESCRIPTION
spec	The specification process TYPE: Process
impl	The implementation process TYPE: Process
mode	Refinement type: - "trace": Trace refinement - "failures": Failures refinement - "fd": Failures-divergences refinement TYPE: str DEFAULT: 'trace'

RETURNS	DESCRIPTION
bool	True if impl refines spec