← Policy gallery

ipl_cert_cases_selected

fix-certification conformance pure_temporal iplimandrafix-certificationtest-generationtest-selection

Region decomposition produces far more cases than can be executed exhaustively. Certification must run a deliberately selected subset of the generated cases — justified by a documented selection strategy and covering the required behaviour classes and risk-prioritised regions — not every generated case, and not an arbitrary few.

Formula

G(CertificationSignoff → P(case_selection_justified ∧ required_classes_covered))

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. ImandraX decomposition is exhaustive by construction, so the full set of regions is typically far too large to run. The certification value comes from a principled selection — representative across behaviour classes, weighted to risk, and always including the invalid and boundary regions — recorded so the choice can be reviewed. Running every case is infeasible; running an arbitrary handful is not certification.

Examples

passes Risk-based selection across all required behaviour classes (incl. invalid regions), rationale recorded → CertificationSignoff

fails CertificationSignoff after running an arbitrary handful of the generated cases with no selection rationale

Use it

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