fix: now analyzing all the transitions to get variables max value, al…

…lowing successful load of real datasets

src/prototype/expression.rs

@@ -16,6 +16,37 @@ pub enum Expression<T> {
     Implies(Box<Expression<T>>, Box<Expression<T>>),
 }
 
+impl<T: Ord + Clone> Expression<T> {
+    pub fn highest_value_used_with_variable(&self, variable_name: &str) -> Option<T> {
+        match self {
+            Expression::Terminal(prop) => {
+                if prop.ci == variable_name {
+                    Some(prop.cn.clone())
+                } else {
+                    None
+                }
+            }
+            Expression::Not(inner) => inner.highest_value_used_with_variable(variable_name),
+            Expression::And(inner) => inner
+                .iter()
+                .filter_map(|expr| expr.highest_value_used_with_variable(variable_name))
+                .max(),
+            Expression::Or(inner) => inner
+                .iter()
+                .filter_map(|expr| expr.highest_value_used_with_variable(variable_name))
+                .max(),
+            Expression::Xor(lhs, rhs) => [lhs, rhs]
+                .iter()
+                .filter_map(|expr| expr.highest_value_used_with_variable(variable_name))
+                .max(),
+            Expression::Implies(lhs, rhs) => [lhs, rhs]
+                .iter()
+                .filter_map(|expr| expr.highest_value_used_with_variable(variable_name))
+                .max(),
+        }
+    }
+}
+
 enum LogicOp {
     Not,
     And,

src/prototype/system_update_fn.rs

@@ -10,6 +10,7 @@ use crate::{
     SymbolicDomain, UnaryIntegerDomain, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, XmlReader,
 };
 
+#[derive(Debug)]
 struct SystemUpdateFn<D: SymbolicDomain<T>, T> {
     penis: std::marker::PhantomData<D>,
     penis_the_second: std::marker::PhantomData<T>,
@@ -68,6 +69,7 @@ impl SystemUpdateFn<UnaryIntegerDomain, u8> {
         self.named_symbolic_domains.values().fold(
             BddPartialValuation::empty(),
             |mut acc, domain| {
+                println!("line 72");
                 domain.encode_bits(&mut acc, &0);
                 acc
             },
@@ -137,24 +139,72 @@ fn load_all_update_fns<XR: XmlReader<BR>, BR: BufRead>(
 fn vars_and_their_max_values(
     vars_and_their_upd_fns: &HashMap<String, UpdateFn<u8>>,
 ) -> HashMap<String, u8> {
+    // todo this will be sufficient once there is a guarantee that the variables
+    // todo  are not used (in comparasions) with values larger than their max_value
+    // todo  (where max_value is determined by the transition function of that variable)
+    // vars_and_their_upd_fns
+    //     .iter()
+    //     .map(|(var_name, upd_fn)| {
+    //         (
+    //             var_name.clone(),
+    //             upd_fn
+    //                 .terms
+    //                 .iter()
+    //                 .map(|(val, _)| val)
+    //                 .chain(std::iter::once(&upd_fn.default))
+    //                 .max() // todo this is not enough
+    //                 .unwrap()
+    //                 .to_owned(),
+    //         )
+    //     })
+    //     .collect()
+
     vars_and_their_upd_fns
         .iter()
-        .map(|(var_name, upd_fn)| {
+        .map(|(var_name, _update_fn)| {
             (
                 var_name.clone(),
-                upd_fn
-                    .terms
-                    .iter()
-                    .map(|(val, _)| val)
-                    .chain(std::iter::once(&upd_fn.default))
-                    .max()
-                    .unwrap()
-                    .to_owned(),
+                get_max_val_of_var_in_all_transitions_including_their_own(
+                    var_name,
+                    vars_and_their_upd_fns,
+                ),
             )
         })
         .collect()
 }
 
+fn get_max_val_of_var_in_all_transitions_including_their_own(
+    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))
+        .max() // todo this is not enough
+        .unwrap()
+        .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(var_name))
+                .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::{SymbolicDomain, UnaryIntegerDomain};
@@ -179,9 +229,24 @@ mod tests {
             .get("todo some existing name")
             .unwrap();
 
+        println!("line 184");
         some_domain.encode_bits(&mut valuation, &1);
     }
 
+    #[test]
+    fn test_bigger() {
+        let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
+            std::fs::File::open("data/bigger.sbml").unwrap(),
+        ));
+
+        crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find start of list");
+
+        let system_update_fn: SystemUpdateFn<UnaryIntegerDomain, u8> =
+            super::SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load system update fn");
+
+        println!("system_update_fn: {:?}", system_update_fn);
+    }
+
     #[test]
     fn test_on_test_data() {
         let mut reader = xml::reader::EventReader::new(std::io::BufReader::new(
@@ -197,6 +262,7 @@ mod tests {
             .named_symbolic_domains
             .get("renamed")
             .unwrap();
+        println!("line 217");
         domain_renamed.encode_bits(&mut valuation, &6);
 
         let res =

src/prototype/update_fn_bdd.rs

@@ -1,4 +1,4 @@
-use std::collections::HashMap;
+use std::{collections::HashMap, fmt::Debug};
 
 use biodivine_lib_bdd::{
     Bdd, BddPartialValuation, BddValuation, BddVariableSet, BddVariableSetBuilder,
@@ -26,6 +26,14 @@ pub struct UpdateFnBdd<D: SymbolicDomain<u8>> {
     pub result_domain: D,
 }
 
+impl<D: SymbolicDomain<u8>> Debug for UpdateFnBdd<D> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        f.debug_struct("UpdateFnBdd")
+            .field("target_var_name", &self.target_var_name)
+            .finish()
+    }
+}
+
 // impl<D: SymbolicDomain<T>, T> From<UpdateFn> for UpdateFnBdd_<D, T> {
 impl<D: SymbolicDomain<u8>> From<UpdateFn<u8>> for UpdateFnBdd<D> {
     fn from(update_fn: UpdateFn<u8>) -> Self {
@@ -177,7 +185,10 @@ fn prop_to_bdd<D: SymbolicDomain<u8>>(
     let val = prop.cn;
 
     match prop.cmp {
-        super::expression::CmpOp::Eq => var.encode_one(bdd_variable_set, &val),
+        super::expression::CmpOp::Eq => {
+            println!("prop ci {:?} of proposition {:?}", prop.ci, prop);
+            var.encode_one(bdd_variable_set, &val)
+        }
         super::expression::CmpOp::Neq => var.encode_one(bdd_variable_set, &val).not(),
         super::expression::CmpOp::Lt => lt(var, bdd_variable_set, val),
         super::expression::CmpOp::Leq => leq(var, bdd_variable_set, val),

src/prototype/update_fn_compiled.rs

@@ -1,6 +1,8 @@
 use std::collections::HashMap;
 
-use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddValuation, BddVariable};
+use biodivine_lib_bdd::{
+    Bdd, BddPartialValuation, BddValuation, BddVariable, BddVariableSet, BddVariableSetBuilder,
+};
 
 use crate::{SymbolicDomain, UpdateFnBdd};
 
@@ -10,6 +12,7 @@ use crate::{SymbolicDomain, UpdateFnBdd};
 // todo for example for UnaryIntegerDomain, T is u8, but i have to specify it like
 // todo UpdateFnCompiled::<UnaryIntegerDomain, u8>::from(update_fn_bdd)
 /// describes, how **single** variable from the system is updated based on the valuation of the system
+#[derive(Debug)]
 pub struct VariableUpdateFnCompiled<D: SymbolicDomain<T>, T> {
     penis: std::marker::PhantomData<T>,
     pub bit_answering_bdds: Vec<(Bdd, BddVariable)>,
@@ -19,12 +22,17 @@ pub struct VariableUpdateFnCompiled<D: SymbolicDomain<T>, T> {
 // todo directly from UpdateFn (not UpdateFnBdd)
 impl<D: SymbolicDomain<u8>> From<UpdateFnBdd<D>> for VariableUpdateFnCompiled<D, u8> {
     fn from(update_fn_bdd: UpdateFnBdd<D>) -> Self {
+        println!("getting debug");
+        println!("update fn bdd: {:?}", update_fn_bdd);
+        println!("got debug");
+
         let mutually_exclusive_terms = to_mutually_exclusive_and_default(
             update_fn_bdd
                 .terms
                 .iter()
                 .map(|(_output, term_bdd)| term_bdd.clone())
                 .collect(),
+            update_fn_bdd.bdd_variable_set.mk_false(),
         );
 
         let outputs = update_fn_bdd
@@ -91,12 +99,16 @@ fn _inspect_outputs_numeric_and_bitwise(numeric_outputs: Vec<u8>, bit_outputs: V
 /// tldr basically succession of guards
 /// adds one more bdd at the end, which is true iff all bdds in the input are false (for given valuation)
 /// todo maybe rewrite this to use fold, but this might be more readable
-fn to_mutually_exclusive_and_default(bdd_succession: Vec<Bdd>) -> Vec<Bdd> {
+fn to_mutually_exclusive_and_default(
+    bdd_succession: Vec<Bdd>,
+    associated_const_false: Bdd,
+) -> Vec<Bdd> {
     if bdd_succession.is_empty() {
-        panic!("got empty bdd succession"); // this should not happen; only using this here
+        return vec![associated_const_false.not()]; // the default value then -> const true
     }
 
-    let mut seen = bdd_succession[0].and_not(&bdd_succession[0]); // const false
+    // let mut seen = bdd_succession[0].and_not(&bdd_succession[0]); // const false
+    let mut seen = associated_const_false;
     let mut mutually_exclusive_terms = Vec::<Bdd>::new();
 
     for term_bdd in bdd_succession {

src/symbolic_domain.rs

@@ -209,8 +209,16 @@ impl SymbolicDomain<u8> for UnaryIntegerDomain {
     fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &u8) {
         // todo do we want this check here or not?
         if value > &(self.variables.len() as u8) {
+            let vars = self
+                .variables
+                .iter()
+                .map(|var| format!("{:?}", var))
+                .collect::<Vec<_>>()
+                .join(", ");
+
             panic!(
-                "Value is too big for this domain; value: {}, domain size: {}",
+                "Value is too big for domain {}; value: {}, domain size: {}",
+                vars,
                 value,
                 self.variables.len()
             )