Home / Concepts / Verification

Verification

ProTest includes a comprehensive verification framework that confirms the correctness of generated covering arrays. Verification checks four aspects of the results — including one of ProTest's most powerful features: transitive constraint analysis.

Coverage Verification

Confirms that every t-way tuple of parameter values appears in at least one test case. This is the core guarantee of a covering array.

• Checks all tuples at the global interaction order
• Checks sub-model tuples at their specified orders
• Reports any missing tuples

Constraint Satisfaction

Confirms that every test case in the results satisfies all defined constraints. No row should violate any constraint.

• Evaluates each constraint against each row
• Supports the full constraint language (IF/THEN/ELSE, comparisons, logical operators)
• Reports any constraint violations with the specific row and constraint

Seed Inclusion

Confirms that all seeded test cases appear in the results.

• Complete seeds must appear exactly as specified
• Partial seeds must have all specified values present in at least one row
• Reports any missing seed matches

Transitive Constraint Analysis

PICT Terminology

PICT internally calls these "derived exclusions" — its ExclusionDeriver resolves all constraints (including their interactions) into a flat list of forbidden parameter-value combinations. ProTest surfaces this concept as transitive constraints and goes further by showing you exactly which constraints chain together to create each derived exclusion.

This is one of ProTest's standout features. When you define constraints, they can interact with each other to create implied exclusions that you never explicitly wrote. ProTest's verification framework detects these transitive constraints and shows you the chain of reasoning.

How It Works

Consider a model with three parameters:

Parameter	Values
Database	MySQL, PostgreSQL
Cache	Redis, Memcached
Queue	RabbitMQ, Kafka

Now add two constraints:

IF [Database] = "MySQL" THEN [Cache] <> "Memcached";
IF [Cache] = "Redis" THEN [Queue] <> "Kafka";

You wrote two constraints, but there is a hidden third one. Here's the chain:

1. If Database = MySQL, then Cache must be Redis (because the first constraint excludes Memcached)
2. If Cache = Redis, then Queue must be RabbitMQ (because the second constraint excludes Kafka)
3. Therefore: If Database = MySQL, then Queue cannot be Kafka — even though you never wrote that constraint

The tuple (Database=MySQL, Queue=Kafka) will be missing from the covering array. Without transitive analysis, this would look like a bug — a missing tuple that should have been covered. But ProTest's verification recognizes it as a transitive constraint and reports it as such, showing you exactly which constraints interact to make this combination infeasible.

What You See in the UI

When you run verification (Ctrl+Shift+V), ProTest analyzes any missing tuples and classifies them:

• Direct constraint — A single constraint explicitly forbids this combination
• Transitive constraint — Multiple constraints interact to make this combination infeasible. ProTest shows which constraints are involved and how they chain together.

If all missing tuples are explained by direct or transitive constraints, the coverage check still passes — the tuples are missing for valid reasons, not due to a generation bug.

Why This Matters

In real-world models with dozens of constraints, transitive interactions are easy to miss. You might have 15 constraints that individually look reasonable, but together they create dozens of implied exclusions you never intended. ProTest makes these hidden relationships visible, helping you:

• Understand your model — See the full picture of what your constraints actually exclude
• Debug unexpected results — When a tuple is missing, know whether it's a constraint interaction or a real problem
• Validate constraint logic — Discover unintended exclusions before they affect your testing

Running Verification

In the UI

Press Ctrl+Shift+V or click Verify in the toolbar. Results appear in the validation summary on the left sidebar, including any transitive constraints with their full chain of reasoning.

Programmatically

The verification framework is available in ProTest.Core through the CoveringArrayVerifier class, which orchestrates all checks including transitive constraint analysis via the TransitiveConstraintAnalyzer.

When Verification Fails

If verification reports issues:

• Missing coverage — Indicates a bug in the generation engine (rare). Try regenerating with a different seed.
• Missing coverage (transitive) — The tuple is infeasible due to constraint interactions. ProTest shows the constraint chain — this is expected behavior, not a bug.
• Constraint violation — The constraint may have been added after generation. Regenerate to include the new constraint.
• Missing seed — The seed may conflict with constraints. Check that the seeded values don't violate any constraint rules.