Skip to content

Commit

Permalink
feat: this needs debugging
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Oct 24, 2023
1 parent 3288104 commit d262349
Show file tree
Hide file tree
Showing 4 changed files with 152 additions and 96 deletions.
157 changes: 109 additions & 48 deletions src/prototype/smart_system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,11 @@ impl<D: SymbolicDomain<u8>> SmartSystemUpdateFn<D, u8> {
pub fn get_whole_state_space_subset(&self) -> Bdd {
self.bdd_variable_set.0.mk_true()
}

/// converts the given bdd into a dot string with names relevant to this system
pub fn bdd_to_dot_string(&self, bdd: &Bdd) -> String {
bdd.to_dot_string(&self.bdd_variable_set, false)
}
}

/// expects the xml reader to be at the start of the <listOfTransitions> element
Expand Down Expand Up @@ -294,6 +299,8 @@ fn get_max_val_of_var_in_all_transitions_including_their_own(

#[cfg(test)]
mod tests {
use xml::EventReader;

use crate::{
prototype::smart_system_update_fn::{self, SmartSystemUpdateFn},
symbolic_domain::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain},
Expand Down Expand Up @@ -339,54 +346,108 @@ mod tests {
println!("dirent = {:?}", dirent);
let dirent = dirent.expect("could not read file");

let xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open(dirent.path()).unwrap(),
));

let mut counting = crate::CountingReader::new(xml);

crate::find_start_of(&mut counting, "listOfTransitions")
.expect("could not find list");

let start = counting.curr_line;

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

println!(
"available variables: {:?}",
smart_system_update_fn.named_symbolic_domains
);

// let currently_reachable = smart_system_update_fn
// .update_fns
// .get("BCat_exp_id99")
// .unwrap()
// .

let empty_subset = smart_system_update_fn.get_empty_state_subset();
let whole_subset = smart_system_update_fn.get_whole_state_space_subset();

let empty_succs = smart_system_update_fn
.transition_under_variable("BCat_exp_id99", &empty_subset);
let whole_succs = smart_system_update_fn
.transition_under_variable("BCat_exp_id99", &whole_subset);

println!("empty succs: {:?}", empty_succs.is_false());
println!("whole succs: {:?}", whole_succs.is_true()); // actually this not being true might be the correct behavior

// let _system_update_fn: SystemUpdateFn<BinaryIntegerDomain<u8>, u8> =
// SystemUpdateFn::try_from_xml(&mut counting)
// .expect("cannot load system update fn");

// println!("file size = {:?}", counting.curr_line);
// println!(
// "just the transitions list = {:?}",
// counting.curr_line - start
// );

// println!("system_update_fn: {:?}", system_update_fn);
let (
smart_empty_succs_dot,
smart_whole_succs_dot,
smart_empty_succs,
smart_whole_succs,
) = {
let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open(dirent.path()).unwrap(),
));

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

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

println!(
"smart const false: {}",
smart_system_update_fn.get_empty_state_subset()
);
println!(
"smart const true: {}",
smart_system_update_fn.get_whole_state_space_subset()
);

let empty_subset = smart_system_update_fn.get_empty_state_subset();
let whole_subset = smart_system_update_fn.get_whole_state_space_subset();

let empty_succs = smart_system_update_fn
.transition_under_variable("BCat_exp_id99", &empty_subset);
let whole_succs = smart_system_update_fn
.transition_under_variable("BCat_exp_id99", &whole_subset);

(
smart_system_update_fn.bdd_to_dot_string(&empty_succs),
smart_system_update_fn.bdd_to_dot_string(&whole_succs),
empty_succs,
whole_succs,
)
};

let (
force_empty_succs_dot,
force_whole_succs_dot,
force_empty_succs,
force_whole_succs,
) = {
let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open(dirent.path()).unwrap(),
));

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

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

println!(
"force const false: {}",
force_system_update_fn.get_empty_state_subset()
);
println!(
"force const true: {}",
force_system_update_fn.get_whole_state_space_subset()
);

let empty_subset = force_system_update_fn.get_empty_state_subset();
let whole_subset = force_system_update_fn.get_whole_state_space_subset();

let empty_succs = force_system_update_fn
.transition_under_variable("BCat_exp_id99", &empty_subset);
let whole_succs = force_system_update_fn
.transition_under_variable("BCat_exp_id99", &whole_subset);

(
force_system_update_fn.bdd_to_dot_string(&empty_succs),
force_system_update_fn.bdd_to_dot_string(&whole_succs),
empty_succs,
whole_succs,
)
};

// assert_eq!(smart_empty_succs, force_empty_succs);
// assert_eq!(smart_whole_succs, force_whole_succs);

assert_eq!(smart_empty_succs_dot, force_empty_succs_dot);

// println!("smart_empty_succs_dot = {:?}", smart_empty_succs_dot);
// println!("force_empty_succs_dot = {:?}", force_empty_succs_dot);

print!("smart_whole_succs_dot = {}", smart_whole_succs_dot);
print!("force_whole_succs_dot = {}", force_whole_succs_dot);

assert_eq!(smart_whole_succs_dot, force_whole_succs_dot); // todo this is the problematic one

// assert!(smart_empty_succs.iff(&force_empty_succs).is_true());
// assert!(smart_whole_succs.iff(&force_whole_succs).is_true());

println!("smart_empty_succs = {:?}", smart_empty_succs);
println!("smart_whole_succs = {:?}", smart_whole_succs);
println!("force_empty_succs = {:?}", force_empty_succs);
println!("force_whole_succs = {:?}", force_whole_succs);
})
}

Expand Down
3 changes: 0 additions & 3 deletions src/prototype/symbolic_transition_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,6 @@ impl<D: SymbolicDomain<T>, T> SymbolicTransitionFn<D, T> {
accumulator = accumulator.and(&the_part_of_the_update_fn);
}

let dot = accumulator.to_dot_string(ctx, false);
println!("dot: {}", dot);

Self {
transition_function: accumulator,
penis: std::marker::PhantomData,
Expand Down
59 changes: 16 additions & 43 deletions src/prototype/system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {

let const_false = current_state.and(&current_state.not()); // used as the start of the fold

let succs = domain
domain
.get_all_possible_values(&self.variable_set)
.into_iter()
.fold(const_false, |acc, possible_value| {
Expand Down Expand Up @@ -153,47 +153,20 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
);

acc.or(&bdd_representing_transition_to_given_value)
});

// for possible_value_of_symbolic_variable in
// domain.get_all_possible_values(&self.variable_set)
// {
// // todo the fact that you have to query two hashmaps with the variables name to get the domain & the update fn suggests it should be refactored
// let update_fn = self
// .update_fns
// .get(transitioned_variable_name.clone())
// .unwrap();

// // todo this one should likely store the domain (and the name?) of the variable it is updating
// // todo because there is some tight coupling between the order of the bit_updating_bdds in update_fn
// // todo and the domain (specifically how the domain encodes given value into (bdd) bits)
// // update_fn.bit_answering_bdds[0].0.ev;

// let bits_of_the_encoded_value =
// domain.encode_bits_into_vec(possible_value_of_symbolic_variable);

// // todo assert the len of the `bits_encoded_value` == count of bdds in `bit_answering_bdds`

// let bdd_representing_transition_to_given_value = update_fn
// .bit_answering_bdds
// .iter()
// .map(|(bit_answering_bdd, _)| bit_answering_bdd)
// .zip(bits_of_the_encoded_value.iter().cloned())
// .fold(
// current_state.clone(),
// |acc, (ith_bit_answering_bdd, ith_expected_bit)| {
// if ith_expected_bit {
// acc.and(ith_bit_answering_bdd)
// } else {
// acc.and(&ith_bit_answering_bdd.not())
// }
// },
// );

// todo!()
// }

todo!()
})
}

pub fn get_empty_state_subset(&self) -> Bdd {
self.variable_set.0.mk_false()
}

pub fn get_whole_state_space_subset(&self) -> Bdd {
self.variable_set.0.mk_true()
}

/// converts the given bdd into a dot string with names relevant to this system
pub fn bdd_to_dot_string(&self, bdd: &Bdd) -> String {
bdd.to_dot_string(&self.variable_set, false)
}
}

Expand Down Expand Up @@ -250,7 +223,7 @@ fn vars_and_their_max_values(
.map(|(var_name, _update_fn)| {
(
var_name.clone(),
get_max_val_of_var_in_all_transitions_including_their_own_and_detect_where_compared_with_larger_than_possible(
get_max_val_of_var_in_all_transitions_including_their_own(
var_name,
vars_and_their_upd_fns,
),
Expand Down
29 changes: 27 additions & 2 deletions src/symbolic_domain.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use biodivine_lib_bdd::{
// todo do not understand what this does, but prevents me from specifying method that does not
// todo take `self`, which is a must if i want to define api for instantiating new symbolic domains
// use dyn_clonable::clonable;
use std::collections::HashSet;
use std::collections::{HashMap, HashSet};

/// Objects implementing `SymbolicDomain` serve as encoders/decoders for their associated type
/// `T` from/into `Bdd` objects.
Expand Down Expand Up @@ -43,7 +43,32 @@ pub trait SymbolicDomain<T>: Clone {
/// instance, lets us inspect...
// todo restrict/define the behavior - should be coupled with encode_bits & get_bdd_variables ordering
fn encode_bits_into_vec(&self, value: T) -> Vec<bool> {
todo!("encode bits into vec not implemented")
let value_encoded_into_partial_valuation = {
let something_to_create_a_partial_valuation_with = self
.symbolic_variables()
.into_iter()
.map(|var| (var, true))
.collect::<Vec<_>>();

let mut partial_valuation =
BddPartialValuation::from_values(&something_to_create_a_partial_valuation_with[..]);

self.encode_bits(&mut partial_valuation, &value);

partial_valuation
};

let bdd_variables_and_their_bit = value_encoded_into_partial_valuation.to_values();

// must correspond to the order of variables in `self.symbolic_variables()`
let bdd_variables_and_their_bit_but_hash_map = bdd_variables_and_their_bit
.into_iter()
.collect::<HashMap<BddVariable, bool>>();

self.symbolic_variables()
.into_iter()
.map(|sym_var| bdd_variables_and_their_bit_but_hash_map[&sym_var])
.collect()
}

/// Decode a value from the provided `BddPartialValuation`.
Expand Down

0 comments on commit d262349

Please sign in to comment.