Package software.amazon.smithy.rulesengine.logic.bdd

Class BddEquivalenceChecker

java.lang.Object

software.amazon.smithy.rulesengine.logic.bdd.BddEquivalenceChecker

public final class BddEquivalenceChecker
extends Object

Verifies functional equivalence between a CFG and its BDD representation.

This verifier uses structural equivalence checking to ensure that both representations produce the same result. When the BDD has fewer than 20 conditions, the checking is exhaustive. When there are more, random samples are checked up to the earlier of max samples being reached or the max duration being reached.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	BddEquivalenceChecker.VerificationException	Exception thrown when verification fails.

Method Summary

Modifier and Type	Method	Description
static BddEquivalenceChecker	of(Cfg cfg, Bdd bdd, List<Condition> conditions, List<Rule> results)
BddEquivalenceChecker	setMaxDuration(Duration timeout)	Sets the maximum amount of time to take for the verification (runs until timeout or max samples met).
BddEquivalenceChecker	setMaxSamples(int maxSamples)	Sets the maximum number of samples to test for large condition sets.
void	verify()	Verifies that the BDD produces identical results to the CFG.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

of

public static BddEquivalenceChecker of(Cfg cfg,
 Bdd bdd,
 List<Condition> conditions,
 List<Rule> results)

setMaxSamples

public BddEquivalenceChecker setMaxSamples(int maxSamples)

Sets the maximum number of samples to test for large condition sets.

Defaults to a max of 1M samples. Set to <= 0 to disable the max.

Parameters:

maxSamples - the maximum number of samples

Returns:

this verifier for method chaining

setMaxDuration

public BddEquivalenceChecker setMaxDuration(Duration timeout)

Sets the maximum amount of time to take for the verification (runs until timeout or max samples met).

Defaults to a 1-minute timeout if not overridden.

Parameters:

timeout - the timeout duration

Returns:

this verifier for method chaining

verify

public void verify()

Verifies that the BDD produces identical results to the CFG.

Throws:

BddEquivalenceChecker.VerificationException - if any discrepancy is found