habedi-work/chase-rs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make property tests deterministic with explicit seeds

Browse Source
This commit is contained in:
Hassan Abedi 2026-03-09 17:49:30 +01:00
parent a8ac280b02
commit b2cfe4763e
1 changed files with 278 additions and 226 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

504
tests/property_tests.rs
View File

@ -1,9 +1,30 @@
//! Property-based tests for the chase algorithm using proptest. //! Property-based tests for the chase algorithm using proptest.
//!
//! All tests use explicit seeds for reproducibility.
use proptest::prelude::*; use proptest::prelude::*;
use proptest::test_runner::{Config, TestRng, TestRunner};
use chase_rs::chase::rule::RuleBuilder; use chase_rs::chase::rule::RuleBuilder;
use chase_rs::{Atom, Instance, Term, chase}; use chase_rs::{Atom, Instance, Substitution, Term, chase};
// =============================================================================
// Test Configuration
// =============================================================================
/// Create a test runner with an explicit seed for reproducibility.
fn seeded_runner(seed: u64, cases: u32) -> TestRunner {
let config = Config::with_cases(cases);
// Create a deterministic seed from u64
let mut seed_bytes = [0u8; 32];
seed_bytes[..8].copy_from_slice(&seed.to_le_bytes());
let rng = TestRng::from_seed(proptest::test_runner::RngAlgorithm::ChaCha, &seed_bytes);
TestRunner::new_with_rng(config, rng)
}
// =============================================================================
// Strategies
// =============================================================================
/// Strategy for generating constant names /// Strategy for generating constant names
fn constant_strategy() -> impl Strategy<Value = String> { fn constant_strategy() -> impl Strategy<Value = String> {
@ -57,335 +78,366 @@ fn instance_strategy() -> impl Strategy<Value = Instance> {
// Property: Chase always terminates // Property: Chase always terminates
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(50))] fn chase_always_terminates() {
const SEED: u64 = 12345;
let mut runner = seeded_runner(SEED, 50);
#[test] runner
fn chase_always_terminates(instance in instance_strategy()) { .run(&instance_strategy(), |instance| {
// Simple rule: P(X) -> Q(X) let rule = RuleBuilder::new()
let rule = RuleBuilder::new() .when("P", vec![Term::var("X")])
.when("P", vec![Term::var("X")]) .then("Q", vec![Term::var("X")])
.then("Q", vec![Term::var("X")]) .build();
.build();
let result = chase(instance, &[rule]); let result = chase(instance, &[rule]);
// Chase should always terminate (either fixpoint or max iterations) prop_assert!(result.terminated || result.steps > 0);
prop_assert!(result.terminated || result.steps > 0); Ok(())
} })
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Chase is monotonic (facts are only added, never removed) // Property: Chase is monotonic (facts are only added, never removed)
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(50))] fn chase_is_monotonic() {
const SEED: u64 = 23456;
let mut runner = seeded_runner(SEED, 50);
#[test] runner
fn chase_is_monotonic(instance in instance_strategy()) { .run(&instance_strategy(), |instance| {
let initial_facts: Vec<_> = instance.iter().cloned().collect(); let initial_facts: Vec<_> = instance.iter().cloned().collect();
let rule = RuleBuilder::new() let rule = RuleBuilder::new()
.when("P", vec![Term::var("X")]) .when("P", vec![Term::var("X")])
.then("Q", vec![Term::var("X")]) .then("Q", vec![Term::var("X")])
.build(); .build();
let result = chase(instance, &[rule]); let result = chase(instance, &[rule]);
// All original facts should still be present for fact in &initial_facts {
for fact in &initial_facts { prop_assert!(
prop_assert!( result.instance.contains(fact),
result.instance.contains(fact), "Original fact {:?} was removed",
"Original fact {:?} was removed", fact fact
); );
} }
// Result should have at least as many facts as the input prop_assert!(result.instance.len() >= initial_facts.len());
prop_assert!(result.instance.len() >= initial_facts.len()); Ok(())
} })
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Fixpoint is stable (running chase again produces no changes) // Property: Fixpoint is stable (running chase again produces no changes)
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(30))] fn fixpoint_is_stable() {
const SEED: u64 = 34567;
let mut runner = seeded_runner(SEED, 30);
#[test] runner
fn fixpoint_is_stable(instance in instance_strategy()) { .run(&instance_strategy(), |instance| {
let rule = RuleBuilder::new() let rule = RuleBuilder::new()
.when("P", vec![Term::var("X")]) .when("P", vec![Term::var("X")])
.then("Q", vec![Term::var("X")]) .then("Q", vec![Term::var("X")])
.build(); .build();
// Run chase to fixpoint let result1 = chase(instance, &[rule.clone()]);
let result1 = chase(instance, &[rule.clone()]); prop_assert!(result1.terminated);
prop_assert!(result1.terminated);
// Run chase again on the result let result2 = chase(result1.instance.clone(), &[rule]);
let result2 = chase(result1.instance.clone(), &[rule]);
// Should terminate immediately with no new facts prop_assert!(result2.terminated);
prop_assert!(result2.terminated); prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes"); prop_assert_eq!(result1.instance.len(), result2.instance.len());
prop_assert_eq!(result1.instance.len(), result2.instance.len()); Ok(())
} })
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: All derived facts are ground (no variables) // Property: All derived facts are ground (no variables)
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(50))] fn all_facts_are_ground() {
const SEED: u64 = 45678;
let mut runner = seeded_runner(SEED, 50);
#[test] runner
fn all_facts_are_ground(instance in instance_strategy()) { .run(&instance_strategy(), |instance| {
let rule = RuleBuilder::new() let rule = RuleBuilder::new()
.when("P", vec![Term::var("X"), Term::var("Y")]) .when("P", vec![Term::var("X"), Term::var("Y")])
.then("R", vec![Term::var("X"), Term::var("Y")]) .then("R", vec![Term::var("X"), Term::var("Y")])
.build(); .build();
let result = chase(instance, &[rule]); let result = chase(instance, &[rule]);
for fact in result.instance.iter() { for fact in result.instance.iter() {
prop_assert!( prop_assert!(fact.is_ground(), "Fact {:?} contains variables", fact);
fact.is_ground(), }
"Fact {:?} contains variables", fact Ok(())
); })
} .unwrap();
}
} }
// ============================================================================= // =============================================================================
// Property: Rules without existentials don't create nulls // Property: Rules without existentials don't create nulls
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(50))] fn no_existentials_means_no_nulls() {
const SEED: u64 = 56789;
let mut runner = seeded_runner(SEED, 50);
#[test] runner
fn no_existentials_means_no_nulls(instance in instance_strategy()) { .run(&instance_strategy(), |instance| {
// Rule with all head variables appearing in body let rule = RuleBuilder::new()
let rule = RuleBuilder::new() .when("P", vec![Term::var("X")])
.when("P", vec![Term::var("X")]) .then("Q", vec![Term::var("X")])
.then("Q", vec![Term::var("X")]) .build();
.build();
let result = chase(instance, &[rule]); let result = chase(instance, &[rule]);
for fact in result.instance.iter() { for fact in result.instance.iter() {
for term in &fact.terms { for term in &fact.terms {
prop_assert!( prop_assert!(
!matches!(term, Term::Null(_)), !matches!(term, Term::Null(_)),
"Found null in fact {:?} but rule has no existentials", fact "Found null in fact {:?} but rule has no existentials",
); fact
);
}
} }
} Ok(())
} })
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Existential rules create exactly one null per trigger // Property: Existential rules create exactly one null per trigger
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(30))] fn existentials_create_unique_nulls() {
const SEED: u64 = 67890;
let mut runner = seeded_runner(SEED, 30);
#[test] runner
fn existentials_create_unique_nulls( .run(&(1usize..5), |num_constants| {
num_constants in 1usize..5 let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
) { let instance: Instance = constants
// Create facts P(c0), P(c1), P(c2), ... with unique constants .iter()
let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect(); .map(|c| Atom::new("P", vec![Term::constant(c)]))
let instance: Instance = constants .collect();
.iter()
.map(|c| Atom::new("P", vec![Term::constant(c)]))
.collect();
// Rule: P(X) -> Q(X, Y) where Y is existential let rule = RuleBuilder::new()
let rule = RuleBuilder::new() .when("P", vec![Term::var("X")])
.when("P", vec![Term::var("X")]) .then("Q", vec![Term::var("X"), Term::var("Y")])
.then("Q", vec![Term::var("X"), Term::var("Y")]) .build();
.build();
let result = chase(instance, &[rule]); let result = chase(instance, &[rule]);
let q_facts: Vec<_> = result.instance.facts_for_predicate("Q"); let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");
// Should have exactly as many Q facts as P facts prop_assert_eq!(q_facts.len(), num_constants);
prop_assert_eq!(q_facts.len(), num_constants);
// Each Q fact should have a null in the second position for fact in &q_facts {
for fact in &q_facts { prop_assert!(
prop_assert!( matches!(fact.terms[1], Term::Null(_)),
matches!(fact.terms[1], Term::Null(_)), "Expected null in second position of {:?}",
"Expected null in second position of {:?}", fact fact
); );
} }
// All nulls should be unique let nulls: Vec<_> = q_facts
let nulls: Vec<_> = q_facts .iter()
.iter() .filter_map(|f| match &f.terms[1] {
.filter_map(|f| match &f.terms[1] { Term::Null(id) => Some(*id),
Term::Null(id) => Some(*id), _ => None,
_ => None, })
}) .collect();
.collect();
let mut unique_nulls = nulls.clone(); let mut unique_nulls = nulls.clone();
unique_nulls.sort(); unique_nulls.sort();
unique_nulls.dedup(); unique_nulls.dedup();
prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique"); prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
} Ok(())
})
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Transitive closure computes correct number of facts // Property: Transitive closure computes correct number of facts
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(20))] fn transitive_closure_chain() {
const SEED: u64 = 78901;
let mut runner = seeded_runner(SEED, 20);
#[test] runner
fn transitive_closure_chain(chain_length in 2usize..6) { .run(&(2usize..6), |chain_length| {
// Create a chain: E(0,1), E(1,2), ..., E(n-1,n) let mut facts = Vec::new();
let mut facts = Vec::new(); for i in 0..chain_length {
for i in 0..chain_length { facts.push(Atom::new(
facts.push(Atom::new( "E",
"E", vec![
vec![Term::constant(format!("{}", i)), Term::constant(format!("{}", i + 1))], Term::constant(format!("{}", i)),
)); Term::constant(format!("{}", i + 1)),
} ],
let instance: Instance = facts.into_iter().collect(); ));
}
let instance: Instance = facts.into_iter().collect();
// E(X,Y) -> T(X,Y) let rule1 = RuleBuilder::new()
let rule1 = RuleBuilder::new() .when("E", vec![Term::var("X"), Term::var("Y")])
.when("E", vec![Term::var("X"), Term::var("Y")]) .then("T", vec![Term::var("X"), Term::var("Y")])
.then("T", vec![Term::var("X"), Term::var("Y")]) .build();
.build();
// T(X,Y), E(Y,Z) -> T(X,Z) let rule2 = RuleBuilder::new()
let rule2 = RuleBuilder::new() .when("T", vec![Term::var("X"), Term::var("Y")])
.when("T", vec![Term::var("X"), Term::var("Y")]) .when("E", vec![Term::var("Y"), Term::var("Z")])
.when("E", vec![Term::var("Y"), Term::var("Z")]) .then("T", vec![Term::var("X"), Term::var("Z")])
.then("T", vec![Term::var("X"), Term::var("Z")]) .build();
.build();
let result = chase(instance, &[rule1, rule2]); let result = chase(instance, &[rule1, rule2]);
prop_assert!(result.terminated); prop_assert!(result.terminated);
let t_facts = result.instance.facts_for_predicate("T"); let t_facts = result.instance.facts_for_predicate("T");
// For a chain of n edges, transitive closure has n*(n+1)/2 pairs let expected = chain_length * (chain_length + 1) / 2;
let expected = chain_length * (chain_length + 1) / 2; prop_assert_eq!(
prop_assert_eq!( t_facts.len(),
t_facts.len(), expected,
expected, "Chain of {} edges should have {} transitive pairs",
"Chain of {} edges should have {} transitive pairs", chain_length,
chain_length, expected
expected );
); Ok(())
} })
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Empty instance with any rules produces empty or stays empty // Property: Empty instance with any rules produces empty or stays empty
// ============================================================================= // =============================================================================
proptest! { #[test]
#[test] fn empty_instance_stays_bounded() {
fn empty_instance_stays_bounded(_seed in 0u64..1000) { const SEED: u64 = 89012;
let instance = Instance::new(); let mut runner = seeded_runner(SEED, 100);
let rule = RuleBuilder::new() runner
.when("P", vec![Term::var("X")]) .run(&(0u64..1000), |_| {
.then("Q", vec![Term::var("X")]) let instance = Instance::new();
.build();
let result = chase(instance, &[rule]); let rule = RuleBuilder::new()
.when("P", vec![Term::var("X")])
.then("Q", vec![Term::var("X")])
.build();
prop_assert!(result.terminated); let result = chase(instance, &[rule]);
prop_assert_eq!(result.steps, 0);
prop_assert!(result.instance.is_empty()); prop_assert!(result.terminated);
} prop_assert_eq!(result.steps, 0);
prop_assert!(result.instance.is_empty());
Ok(())
})
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Substitution application is idempotent for ground terms // Property: Substitution application is idempotent for ground terms
// ============================================================================= // =============================================================================
use chase_rs::Substitution; #[test]
fn substitution_ground_term_unchanged() {
const SEED: u64 = 90123;
let mut runner = seeded_runner(SEED, 100);
proptest! { runner
#![proptest_config(ProptestConfig::with_cases(100))] .run(&constant_strategy(), |c| {
let term = Term::constant(&c);
let mut subst = Substitution::new();
subst.bind("X".to_string(), Term::constant("other"));
#[test] let result = subst.apply_term(&term);
fn substitution_ground_term_unchanged(c in constant_strategy()) {
let term = Term::constant(&c);
let mut subst = Substitution::new();
subst.bind("X".to_string(), Term::constant("other"));
let result = subst.apply_term(&term); prop_assert_eq!(
result,
prop_assert_eq!(result, term, "Ground term should be unchanged by substitution"); term,
} "Ground term should be unchanged by substitution"
);
Ok(())
})
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Substitution correctly replaces variables // Property: Substitution correctly replaces variables
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(100))] fn substitution_replaces_variable() {
const SEED: u64 = 11111;
let mut runner = seeded_runner(SEED, 100);
#[test] runner
fn substitution_replaces_variable( .run(
var in variable_strategy(), &(variable_strategy(), constant_strategy()),
replacement in constant_strategy() |(var, replacement)| {
) { let term = Term::var(&var);
let term = Term::var(&var); let mut subst = Substitution::new();
let mut subst = Substitution::new(); subst.bind(var.clone(), Term::constant(&replacement));
subst.bind(var.clone(), Term::constant(&replacement));
let result = subst.apply_term(&term); let result = subst.apply_term(&term);
prop_assert_eq!( prop_assert_eq!(
result, result,
Term::constant(&replacement), Term::constant(&replacement),
"Variable should be replaced" "Variable should be replaced"
); );
} Ok(())
},
)
.unwrap();
} }
// ============================================================================= // =============================================================================
// Property: Atom arity is preserved through substitution // Property: Atom arity is preserved through substitution
// ============================================================================= // =============================================================================
proptest! { #[test]
#![proptest_config(ProptestConfig::with_cases(50))] fn substitution_preserves_arity() {
const SEED: u64 = 22222;
let mut runner = seeded_runner(SEED, 50);
#[test] let strategy = (
fn substitution_preserves_arity( predicate_strategy(),
pred in predicate_strategy(), prop::collection::vec(variable_strategy(), 1..4),
vars in prop::collection::vec(variable_strategy(), 1..4), constant_strategy(),
replacement in constant_strategy() );
) {
let atom = Atom::new(
&pred,
vars.iter().map(|v| Term::var(v)).collect(),
);
let mut subst = Substitution::new(); runner
for var in &vars { .run(&strategy, |(pred, vars, replacement)| {
subst.bind(var.clone(), Term::constant(&replacement)); let atom = Atom::new(&pred, vars.iter().map(|v| Term::var(v)).collect());
}
let result = subst.apply_atom(&atom); let mut subst = Substitution::new();
for var in &vars {
subst.bind(var.clone(), Term::constant(&replacement));
}
prop_assert_eq!(result.arity(), atom.arity()); let result = subst.apply_atom(&atom);
prop_assert_eq!(result.predicate, atom.predicate);
} prop_assert_eq!(result.arity(), atom.arity());
prop_assert_eq!(result.predicate, atom.predicate);
Ok(())
})
.unwrap();
} }