Skip to content

Commit

Permalink
feat: provided a way to detect propositions that do not make sense
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Oct 21, 2023
1 parent 12e9747 commit ceaddcb
Show file tree
Hide file tree
Showing 3 changed files with 140 additions and 31 deletions.
76 changes: 75 additions & 1 deletion src/prototype/expression.rs
Original file line number Diff line number Diff line change
@@ -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;

Expand Down Expand Up @@ -47,6 +47,80 @@ impl<T: Ord + Clone> Expression<T> {
}
}

impl<T: Ord + Clone + Debug> Expression<T> {
/// 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<T> {
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,
Expand Down
90 changes: 63 additions & 27 deletions src/prototype/system_update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
),
Expand All @@ -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
Expand All @@ -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<String, UpdateFn<u8>>,
) -> 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::{
Expand Down Expand Up @@ -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<BinaryIntegerDomain<u8>, u8> =
super::SystemUpdateFn::try_from_xml(&mut counting)
.expect("cannot load system update fn");
let _system_update_fn: SystemUpdateFn<BinaryIntegerDomain<u8>, 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]
Expand Down
5 changes: 2 additions & 3 deletions src/symbolic_domain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -396,9 +396,8 @@ impl SymbolicDomain<u8> for BinaryIntegerDomain<u8> {
// 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
)
}

Expand Down

0 comments on commit ceaddcb

Please sign in to comment.