Skip to content

Commit

Permalink
feat: well it works
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Nov 5, 2023
1 parent 8a1bb2f commit 1682a2c
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 6 deletions.
6 changes: 2 additions & 4 deletions src/prototype/smart_system_update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1549,8 +1549,6 @@ mod tests {
fn test_preds_kinda_inclusive() {
std::fs::read_dir("data/large")
.expect("could not read dir")
.skip(4)
.take(1)
.for_each(|dirent| {
println!("dirent = {:?}", dirent);
let filepath = dirent.expect("could not read file").path();
Expand Down Expand Up @@ -1638,10 +1636,10 @@ mod tests {
// let res =
// let var_names = &var_names[..1];
// var_names.par_iter().for_each(|var_name| {
var_names.iter().skip(1).take(1).for_each(|var_name| {
var_names.iter().for_each(|var_name| {
// let smart_bdd_force_bdd_tuples = &smart_bdd_force_bdd_tuples[..1];
// smart_bdd_force_bdd_tuples.par_iter().for_each(
smart_bdd_force_bdd_tuples.iter().take(1).for_each(
smart_bdd_force_bdd_tuples.iter().for_each(
|(name, smart_set_of_states, force_set_of_states)| {
// println!("comparing bdds of {}", name);
let smart_preds = smart_system_update_fn
Expand Down
48 changes: 46 additions & 2 deletions src/prototype/system_update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -497,7 +497,7 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
.zip(its_bits)
.collect::<Vec<_>>();
let target_set_of_states_with_known_value_of_target_var =
target_set_of_states.select(&vars_and_their_bits[..]);
target_set_of_states.restrict(&vars_and_their_bits[..]);

let target_set_of_states_with_known_value_but_relaxed =
target_set_of_states_with_known_value_of_target_var
Expand All @@ -519,7 +519,7 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {

// fill the spot with possible value
let with_specific_value = target_set_of_states_with_known_value_but_relaxed
.select(&vars_and_their_bits[..]);
.restrict(&vars_and_their_bits[..]);

acc.or(&with_specific_value)
},
Expand Down Expand Up @@ -554,6 +554,50 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
)
}

pub fn predecessors_attempt_3(
&self,
transitioned_variable_name: &str,
target_set_of_states: &Bdd,
) -> Bdd {
let sym_dom = self
.named_symbolic_domains
.get(transitioned_variable_name)
.expect("unknown variable name");

let bit_updating_bdds = self
.update_fns
.get(transitioned_variable_name)
.unwrap()
.bit_answering_bdds
.iter()
.map(|(bdd, var)| (var, bdd))
.collect::<HashMap<_, _>>();

let ordered_vars_and_bdds = sym_dom
.symbolic_variables()
.into_iter()
.map(|var| (var, (*bit_updating_bdds.get(&var).unwrap()).clone()));

let const_false = target_set_of_states.and(&target_set_of_states.not());

sym_dom
.get_all_possible_values(&self.bdd_variable_set)
.into_iter()
.fold(const_false.clone(), |acc, one_of_possible_values| {
let bits = sym_dom.encode_bits_into_vec(one_of_possible_values);
let target_set_of_states_with_known_value_of_target_var = target_set_of_states
.select(
&ordered_vars_and_bdds
.clone()
.map(|(var, _)| var)
.zip(bits)
.collect::<Vec<_>>()[..],
);

todo!()
})
}

pub fn get_empty_state_subset(&self) -> Bdd {
self.bdd_variable_set.0.mk_false()
}
Expand Down

0 comments on commit 1682a2c

Please sign in to comment.