Skip to content

Commit

Permalink
fix: bruh off by one error fix making the whole preds/succs tests pass
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Dec 14, 2023
1 parent be302eb commit 8c1441d
Show file tree
Hide file tree
Showing 3 changed files with 56 additions and 49 deletions.
4 changes: 2 additions & 2 deletions src/symbolic_domains/symbolic_domain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -390,7 +390,7 @@ impl SymbolicDomain<u8> for BinaryIntegerDomain<u8> {
}

fn unit_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
(0..self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
(0..=self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
acc.or(&self.encode_one(bdd_variable_set, &val))
})
}
Expand Down Expand Up @@ -514,7 +514,7 @@ impl SymbolicDomain<u8> for GrayCodeIntegerDomain<u8> {
}

fn unit_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
(0..self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
(0..=self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
acc.or(&self.encode_one(bdd_variable_set, &val))
})
}
Expand Down
4 changes: 2 additions & 2 deletions src/update/update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,9 @@ where
{
/// ordered by variable name // todo add a method to get the update function by name (hash map or binary search)
pub update_fns: Vec<(String, (VariableUpdateFn, D))>, // todo do not keep pub; just here for testing
bdd_variable_set: DebugIgnore<BddVariableSet>,
pub bdd_variable_set: DebugIgnore<BddVariableSet>, // todo do not keep pub
_marker: std::marker::PhantomData<T>,
pub cache: Vec<String>,
pub cache: Vec<String>, // todo do not keep at all; just here for testing/debug
}

impl<DO, T> SystemUpdateFn<DO, T>
Expand Down
97 changes: 52 additions & 45 deletions tests/some_test.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,12 @@
#![allow(dead_code)]

use biodivine_lib_bdd::Bdd;
use biodivine_lib_logical_models::prelude as bio;
use biodivine_lib_logical_models::prelude::{
self as bio, old_symbolic_domain::SymbolicDomain, symbolic_domain::SymbolicDomain as _,
};

type OldDomain = bio::old_symbolic_domain::GrayCodeIntegerDomain<u8>;
type NewDomain = bio::symbolic_domain::GrayCodeIntegerDomain<u8>;
type OldDomain = bio::old_symbolic_domain::BinaryIntegerDomain<u8>;
type NewDomain = bio::symbolic_domain::BinaryIntegerDomain<u8>;

struct TheFourImpls<D, OD>
where
Expand Down Expand Up @@ -662,6 +664,7 @@ fn check_specific() {
#[test]
fn predecessors_consistency_check() {
let mut i = 0usize;
let mut whole_test_count = 0usize;

loop {
std::fs::read_dir("data/large")
Expand Down Expand Up @@ -699,57 +702,61 @@ fn predecessors_consistency_check() {
"the new impls should be the same"
);

assert!(initial_state.are_same(&the_four), "initial states are same");

let transitioned = the_four.predecessors_async(variable, initial_state);

// todo currently, there is a discrepancy between the old and new impls
// todo old are unit-set-pruned -> correct
// assert!(
// transitioned.old_are_same(&the_four),
// "the old impls should be the same"
// );

// if !transitioned.new_are_same(&the_four) {
// // println!("old are not the same");
// println!(
// "new dumb bdd = {}",
// the_four
// .new_dumb
// .bdd_to_dot_string(&transitioned.new_dumb_bdd)
// );
// println!(
// "new smart bdd = {}",
// the_four
// .new_smart
// .bdd_to_dot_string(&transitioned.new_smart_bdd)
// );
// }
let old_dumb_const_true = the_four.old_dumb.bdd_variable_set.mk_true();
let unit_set_old_dumb = the_four
.old_dumb
.update_fns
.iter()
.find(|_| true)
.map(|(_, update_fn)| {
update_fn.named_symbolic_domains.iter().fold(
old_dumb_const_true,
|acc, (_, domain)| {
acc.and(
&domain
.unit_collection(&the_four.old_dumb.bdd_variable_set),
)
},
)
})
.unwrap();

let unit_set_old_dumb_str =
the_four.old_dumb.bdd_to_dot_string(&unit_set_old_dumb);
// println!("unit set old dumb: {}", unit_set_old_dumb_str);

let new_dumb_const_true = the_four.new_dumb.bdd_variable_set.mk_true();
let unit_set_new_dumb = the_four.new_dumb.update_fns.iter().fold(
new_dumb_const_true,
|acc, (_, (_, domain))| {
acc.and(&domain.unit_collection(&the_four.new_dumb.bdd_variable_set))
},
);

// assert!(
// transitioned.new_are_same(&the_four),
// "the new impls should be the same"
// );
let unit_set_new_dumb_str =
the_four.new_dumb.bdd_to_dot_string(&unit_set_new_dumb);

// assert!(
// transitioned.smart_are_same(&the_four),
// "the smart impls should be the same"
// );
assert!(
unit_set_old_dumb_str == unit_set_new_dumb_str,
"the unit sets should be the same"
);

// assert!(
// transitioned.dumb_are_same(&the_four),
// "the dumb impls should be the same"
// );
// assert!(false, "ok");

// assert!(transitioned.old_are_same(&the_four), "old");
assert!(initial_state.are_same(&the_four), "initial states are same");

// assert!(transitioned.dumb_are_same(&the_four), "dumb");
let transitioned = the_four.successors_async(variable, initial_state);

assert!(transitioned.new_are_same(&the_four), "all are same");
assert!(transitioned.are_same(&the_four), "all are same");

println!("predecessors count = {} were the same", i);
println!(
"predecessors count = {} were the same; whole test {}",
i, whole_test_count
);
i += 1;
}
});

whole_test_count += 1;
}
}

0 comments on commit 8c1441d

Please sign in to comment.