Skip to content

Commit

Permalink
feat: some bs idk
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Nov 1, 2023
1 parent 3567d5f commit 8975485
Show file tree
Hide file tree
Showing 2 changed files with 158 additions and 62 deletions.
77 changes: 64 additions & 13 deletions src/prototype/smart_system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1003,7 +1003,7 @@ mod tests {

crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list");

let smart_system_update_fn: SmartSystemUpdateFn<BinaryIntegerDomain<u8>, u8> =
let smart_system_update_fn: SmartSystemUpdateFn<UnaryIntegerDomain, u8> =
SmartSystemUpdateFn::try_from_xml(&mut xml)
.expect("cannot load smart system update fn");

Expand All @@ -1017,29 +1017,80 @@ mod tests {

crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list");

let force_system_update_fn: SystemUpdateFn<BinaryIntegerDomain<u8>, u8> =
let force_system_update_fn: SystemUpdateFn<UnaryIntegerDomain, u8> =
SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn");

force_system_update_fn
};

let smart_zero_bdd =
// let smart_zero_bdd =
// smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
// // let smart_one_bdd =
// // smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 1);
// // let smart_zero_or_one_bdd = smart_zero_bdd.or(&smart_one_bdd);

// let force_zero_bdd =
// force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
// // let force_one_bdd =
// // force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 1);
// // let force_zero_or_one_bdd = force_zero_bdd.or(&force_one_bdd);

let smart_zero_p =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
let smart_one_bdd =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 1);
let smart_zero_or_one_bdd = smart_zero_bdd.or(&smart_one_bdd);
let smart_zero_q =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let smart_zero_p_and_q = smart_zero_p.and(&smart_zero_q);

let force_zero_bdd =
let force_zero_p =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
let force_one_bdd =
let force_zero_q =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let force_zero_p_and_q = force_zero_p.and(&force_zero_q);

// let smart_preds = smart_system_update_fn.predecessors_under_variable("p", &smart_zero_bdd);

// let force_preds = force_system_update_fn.predecessors_under_variable("p", &smart_zero_bdd);

let smart_preds =
smart_system_update_fn.predecessors_under_variable("p", &smart_zero_p_and_q);
let force_preds =
force_system_update_fn.predecessors_under_variable("p", &force_zero_p_and_q);

let smart_one_p =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 1);
let smart_zero_q =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let smart_one_p_and_zero_q = smart_one_p.and(&smart_zero_q);

let force_one_p =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 1);
let force_zero_or_one_bdd = force_zero_bdd.or(&force_one_bdd);
let force_zero_q =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let force_one_p_and_zero_q = force_one_p.and(&force_zero_q);

let smart_preds =
smart_system_update_fn.predecessors_under_variable("p", &smart_one_p_and_zero_q);

let force_preds =
force_system_update_fn.predecessors_under_variable("p", &force_one_p_and_zero_q);

let smart_zero_p =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
let smart_zero_q =
smart_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let smart_zero_p_and_q = smart_zero_p.and(&smart_zero_q);

let force_zero_p =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("p", 0);
let force_zero_q =
force_system_update_fn.get_bdd_with_specific_var_set_to_specific_value("q", 0);
let force_zero_p_and_q = force_zero_p.and(&force_zero_q);

let smart_preds =
smart_system_update_fn.predecessors_under_variable("p", &smart_zero_or_one_bdd);
smart_system_update_fn.predecessors_under_variable("p", &smart_zero_p_and_q);

let force_preds =
force_system_update_fn.predecessors_under_variable("p", &force_zero_or_one_bdd);
force_system_update_fn.predecessors_under_variable("p", &force_zero_p_and_q);

let the_two_transitioned = format!(
"{}\n{}",
Expand Down Expand Up @@ -1266,8 +1317,8 @@ mod tests {
let smart_transitioned = smart_system_update_fn
.transition_under_variable(var_name, smart_set_of_states);

let smart_predecessors_of_successors = smart_system_update_fn
.predecessors_under_variable(&var_name, &smart_transitioned);
// let smart_predecessors_of_successors = smart_system_update_fn
// .predecessors_under_variable(&var_name, &smart_transitioned);

// assert!(smart_set_of_states
// .iff(&smart_predecessors_of_successors)
Expand Down
143 changes: 94 additions & 49 deletions src/prototype/system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,6 +278,31 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {

// todo remove all the redundant cloning of transitioned_variable_name in the above funciton

let var_upd_fn = self // todo here
.update_fns
.get(transitioned_variable_name.clone())
.unwrap();

let vars_and_their_updating_bdds = var_upd_fn // todo here
.bit_answering_bdds
.iter()
.map(|(bdd, variable)| (variable, bdd))
.collect::<HashMap<_, _>>();

// let vars_and_their_bits = domain
// .symbolic_variables()
// .into_iter()
// .zip(bits_of_the_encoded_value.clone())
// .collect::<Vec<_>>();

// // must order the bit-answering bdds the way the variables are ordered in the domain
// let correctly_ordered_bit_answered_bdds = vars_and_their_bits
// .iter()
// .map(|(bdd_variable, _)| {
// vars_and_their_updating_bdds.get(bdd_variable).unwrap() // todo here
// })
// .collect::<Vec<_>>();

let target_var_sym_dom = self
.named_symbolic_domains
.get(transitioned_variable_name)
Expand Down Expand Up @@ -323,8 +348,6 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
)
});

let name = self.update_fns.get("");

let states_with_known_val_of_target_var_and_their_predecessors =
current_state_split_by_value_of_target_var.map(
|(fixed_val_bits, set_of_states_with_var_with_specific_bits)| {
Expand All @@ -349,58 +372,80 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
acc.or(&current_state_with_specific_value_of_target_var)
});

let vars_and_their_bits = target_var_sym_dom
.clone()
.symbolic_variables()
.into_iter()
.zip(fixed_val_bits.clone())
.collect::<Vec<_>>();

// must order the bit-answering bdds the way the variables are ordered in the domain
let correctly_ordered_bit_answered_bdds = vars_and_their_bits
.iter()
.map(|(bdd_variable, _)| {
vars_and_their_updating_bdds.get(bdd_variable).unwrap()
// todo here
})
.collect::<Vec<_>>();

// todo abstract the function `set_of_those_states_that_transition_to_specific_value_of_specific_variable`
// let those_transitioning_to_target =
target_var_sym_dom
.symbolic_variables()
// target_var_sym_dom
// .symbolic_variables()
// .into_iter()
// .zip(fixed_val_bits)
correctly_ordered_bit_answered_bdds
.into_iter()
.zip(fixed_val_bits)
.fold(relaxed_value_of_target_var, |acc, (bdd_var, bit_val)| {
let name_of_this_var = self.bdd_variable_set.name_of(bdd_var);
let bdd_updating_bdd_var = {
let aux = self.update_fns.get(&name_of_this_var);
if aux.is_none() {
panic!(
"could not find variable `{}`; only available: `{}`",
name_of_this_var,
// self.bdd_variable_set
// .0
// .variables()
// .iter()
// .map(|var| self
// .bdd_variable_set
// .name_of(var.to_owned()))
// .collect::<Vec<_>>()
// .join(", ")
self.update_fns
.keys()
.cloned()
.collect::<Vec<_>>()
.join(", ")
);
.fold(
relaxed_value_of_target_var,
|acc, (bit_updating_bdd, bit_val)| {
// let name_of_this_var = self.bdd_variable_set.name_of(bdd_var);
// let bdd_updating_bdd_var = {
// let aux = self.update_fns.get(&name_of_this_var);
// if aux.is_none() {
// panic!(
// "could not find variable `{}`; only available: `{}`",
// name_of_this_var,
// // self.bdd_variable_set
// // .0
// // .variables()
// // .iter()
// // .map(|var| self
// // .bdd_variable_set
// // .name_of(var.to_owned()))
// // .collect::<Vec<_>>()
// // .join(", ")
// self.update_fns
// .keys()
// .cloned()
// .collect::<Vec<_>>()
// .join(", ")
// );
// }
// aux.unwrap()
// };
// // todo this should already be zipped with the iterator -> would be O(n) instead of O(n^2)
// let bdd_updating_specific_bit = &bdd_updating_bdd_var
// .bit_answering_bdds
// .clone()
// .into_iter()
// .find_map(|(bdd, maybe_target_bdd_var)| {
// if bdd_var == maybe_target_bdd_var {
// Some(bdd)
// } else {
// None
// }
// })
// .unwrap();

if bit_val {
acc.and(bit_updating_bdd)
} else {
acc.and(&bit_updating_bdd.not())
}
aux.unwrap()
};
// todo this should already be zipped with the iterator -> would be O(n) instead of O(n^2)
let bdd_updating_specific_bit = &bdd_updating_bdd_var
.bit_answering_bdds
.clone()
.into_iter()
.find_map(|(bdd, maybe_target_bdd_var)| {
if bdd_var == maybe_target_bdd_var {
Some(bdd)
} else {
None
}
})
.unwrap();

if bit_val {
acc.and(bdd_updating_specific_bit)
} else {
acc.and(&bdd_updating_specific_bit.not())
}
})
},
)
},
);

Expand Down

0 comments on commit 8975485

Please sign in to comment.