← Policy gallery

ipl_cert_cases_from_decomposition

fix-certification conformance scoped_temporal iplimandrafix-certificationtest-generationconformance

The certification cases a counterparty is tested against must be generated from the IPL model by region decomposition — each case traceable to a symbolic region of the model — rather than hand-written ad hoc.

Formula

G(CertificationCase → P_chain(RegionDecomposition ∧ ipl_model_valid))

Hover any operator or symbol for what it means.

Requires a reasoner

This policy is satisfied by verification from imandrax — an automated-reasoning tool in the reasoner registry.

Why it matters

Case Generation & Selection. Region Decomposition — computed by the ImandraX reasoner — turns the IPL model's infinite state space into a finite, exhaustive set of symbolic regions, and each region yields one certification case. A case whose lineage does not trace back to a decomposition of a valid model is not grounded in the spec and can silently miss whole regions of behaviour.

Examples

passes RegionDecomposition(valid IPL model) → generated CertificationCase

fails CertificationCase hand-authored with no decomposition of the IPL model in its lineage

Use it

ponens policies add ipl_cert_cases_from_decomposition --into ./trace.json
ponens trace check ./trace.json