diff --git a/src/prototype/expression.rs b/src/prototype/expression.rs index 7e6515f..84ec497 100644 --- a/src/prototype/expression.rs +++ b/src/prototype/expression.rs @@ -1,4 +1,4 @@ -use std::{io::BufRead, str::FromStr}; +use std::{fmt::Debug, io::BufRead, str::FromStr}; use thiserror::Error; use xml::reader::XmlEvent; @@ -47,6 +47,80 @@ impl Expression { } } +impl Expression { + /// function works entirely the same as `highest_value_used_with_variable` but provides debug prints + /// displaying all the propositions that compare the variable with higher values than its domain is + pub fn highest_value_used_with_variable_detect_higher_than_exected( + &self, + variable_name: &str, + expected_highest: T, + ) -> Option { + match self { + Expression::Terminal(prop) => { + if prop.ci == variable_name { + let value_being_compared_to = prop.cn.clone(); + + if value_being_compared_to > expected_highest { + println!( + "[debug] variable {} only can take values in the [0; {:?}], but is being compared to with {:?} in proposition {:?}", + prop.ci, + expected_highest, + value_being_compared_to, + self + ) + } + + Some(prop.cn.clone()) + } else { + None + } + } + // Expression::Not(inner) => inner.highest_value_used_with_variable(variable_name), + Expression::Not(inner) => inner + .highest_value_used_with_variable_detect_higher_than_exected( + variable_name, + expected_highest, + ), + Expression::And(inner) => inner + .iter() + .filter_map(|expr| { + expr.highest_value_used_with_variable_detect_higher_than_exected( + variable_name, + expected_highest.clone(), + ) + }) + .max(), + Expression::Or(inner) => inner + .iter() + .filter_map(|expr| { + expr.highest_value_used_with_variable_detect_higher_than_exected( + variable_name, + expected_highest.clone(), + ) + }) + .max(), + Expression::Xor(lhs, rhs) => [lhs, rhs] + .iter() + .filter_map(|expr| { + expr.highest_value_used_with_variable_detect_higher_than_exected( + variable_name, + expected_highest.clone(), + ) + }) + .max(), + Expression::Implies(lhs, rhs) => [lhs, rhs] + .iter() + .filter_map(|expr| { + expr.highest_value_used_with_variable_detect_higher_than_exected( + variable_name, + expected_highest.clone(), + ) + }) + .max(), + } + } +} + enum LogicOp { Not, And, diff --git a/src/prototype/system_update_fn.rs b/src/prototype/system_update_fn.rs index f923a59..39403cc 100644 --- a/src/prototype/system_update_fn.rs +++ b/src/prototype/system_update_fn.rs @@ -158,7 +158,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( + get_max_val_of_var_in_all_transitions_including_their_own_and_detect_where_compared_with_larger_than_possible( var_name, vars_and_their_upd_fns, ), @@ -180,9 +180,9 @@ fn get_max_val_of_var_in_all_transitions_including_their_own( .terms .iter() .map(|(val, _)| val) - .chain(std::iter::once(&update_fns.get(var_name).unwrap().default)) + .chain(std::iter::once(&update_fns.get(var_name).unwrap().default)) // add the value of default term .max() // todo this is not enough - .unwrap() + .unwrap() // safe unwrap; at least default terms value always present .to_owned(); let max_in_terms = update_fns @@ -202,6 +202,44 @@ fn get_max_val_of_var_in_all_transitions_including_their_own( } } +fn get_max_val_of_var_in_all_transitions_including_their_own_and_detect_where_compared_with_larger_than_possible( + var_name: &str, + update_fns: &HashMap>, +) -> u8 { + let max_in_its_update_fn = update_fns + .get(var_name) + .unwrap() + .terms + .iter() + .map(|(val, _)| val) + .chain(std::iter::once(&update_fns.get(var_name).unwrap().default)) // add the value of default term + .max() + .unwrap() // safe unwrap; at least the default terms value always present + .to_owned(); + + let max_in_terms = update_fns + .values() + .filter_map(|update_fn| { + update_fn + .terms + .iter() + .filter_map(|term| { + term.1 + .highest_value_used_with_variable_detect_higher_than_exected( + var_name, + max_in_its_update_fn, + ) + }) + .max() + }) + .max(); + + match max_in_terms { + None => max_in_its_update_fn, + Some(max_in_terms) => std::cmp::max(max_in_its_update_fn, max_in_terms), + } +} + #[cfg(test)] mod tests { use crate::{ @@ -261,37 +299,35 @@ mod tests { #[test] fn test_all_bigger() { - for _ in 0..10 { - std::fs::read_dir("data/large") - .expect("could not read dir") - .for_each(|dirent| { - println!("dirent = {:?}", dirent); - let dirent = dirent.expect("could not read file"); + std::fs::read_dir("data/large") + .expect("could not read dir") + .for_each(|dirent| { + 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 xml = xml::reader::EventReader::new(std::io::BufReader::new( + std::fs::File::open(dirent.path()).unwrap(), + )); - let mut counting = crate::CountingReader::new(xml); + let mut counting = crate::CountingReader::new(xml); - crate::find_start_of(&mut counting, "listOfTransitions") - .expect("could not find list"); + crate::find_start_of(&mut counting, "listOfTransitions") + .expect("could not find list"); - let start = counting.curr_line; + let start = counting.curr_line; - let _system_update_fn: SystemUpdateFn, u8> = - super::SystemUpdateFn::try_from_xml(&mut counting) - .expect("cannot load system update fn"); + let _system_update_fn: SystemUpdateFn, u8> = + super::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!("file size = {:?}", counting.curr_line); + println!( + "just the transitions list = {:?}", + counting.curr_line - start + ); - // println!("system_update_fn: {:?}", system_update_fn); - }) - } + // println!("system_update_fn: {:?}", system_update_fn); + }) } #[test] diff --git a/src/symbolic_domain.rs b/src/symbolic_domain.rs index ed227e3..ba1b452 100644 --- a/src/symbolic_domain.rs +++ b/src/symbolic_domain.rs @@ -396,9 +396,8 @@ impl SymbolicDomain for BinaryIntegerDomain { // todo do we want this check here or not? if value > &self.max_value { panic!( - "Value is too big for this domain; value: {}, domain size: {}", - value, - self.variables.len() + "Value is too big for this domain; value: {}, domain can only hold values in range [0, {}] (inlusive)", + value, self.max_value ) }