From dcda5271737ee31c20a95c4a6632753aeb19f774 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Chud=C3=AD=C4=8Dek?= Date: Sun, 12 Nov 2023 00:52:52 +0100 Subject: [PATCH] refactor: fixed the problem with the public exporting --- examples/reachability.rs | 7 +- src/lib.rs | 15 ++-- src/prototype/expression.rs | 2 +- src/prototype/mod.rs | 4 +- src/prototype/reachability.rs | 74 +++++++++++++---- src/prototype/smart_system_update_fn.rs | 104 +++++++++++------------- src/prototype/symbolic_transition_fn.rs | 6 +- src/prototype/system_update_fn.rs | 45 +++++----- src/prototype/update_fn.rs | 5 +- src/prototype/update_fn_bdd.rs | 10 +-- src/prototype/update_fn_compiled.rs | 17 ++-- src/prototype/utils.rs | 51 ++++++++---- src/test_utils.rs | 83 ++++++++++++------- 13 files changed, 256 insertions(+), 167 deletions(-) diff --git a/examples/reachability.rs b/examples/reachability.rs index 39a8374..d7fd0fb 100644 --- a/examples/reachability.rs +++ b/examples/reachability.rs @@ -1,4 +1,7 @@ -use biodivine_lib_logical_models::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, reachability_benchmark, UnaryIntegerDomain}; +use biodivine_lib_logical_models::{ + reachability_benchmark, BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, + UnaryIntegerDomain, +}; fn main() { let args = std::env::args().collect::>(); @@ -12,4 +15,4 @@ fn main() { "gray" | "grey" => reachability_benchmark::>(sbml_path.as_str()), _ => panic!("Unknown representation: {}.", representation), } -} \ No newline at end of file +} diff --git a/src/lib.rs b/src/lib.rs index 55355f7..63cec42 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,3 +1,5 @@ +pub use prototype::reachability_benchmark; // this is the only one that should be publicly exported for now + /// A private module which stores the implementation of the traits/structures relevant for /// symbolic encoding of logical models. /// @@ -11,14 +13,14 @@ mod symbolic_domain; pub mod test_utils; pub use symbolic_domain::{ + BinaryIntegerDomain, + GrayCodeIntegerDomain, + PetriNetIntegerDomain, // todo uncomment one those working // GenericIntegerDomain, // GenericStateSpaceDomain, SymbolicDomain, UnaryIntegerDomain, - PetriNetIntegerDomain, - BinaryIntegerDomain, - GrayCodeIntegerDomain, }; pub fn add(x: i32, y: i32) -> i32 { @@ -27,10 +29,11 @@ pub fn add(x: i32, y: i32) -> i32 { // expose the prototype module mod prototype; -pub use prototype::*; #[cfg(test)] mod tests { + use crate::prototype::{Expression, UpdateFn}; + use super::add; #[test] @@ -138,7 +141,7 @@ mod tests { println!("start element {:?}", name); if name.local_name == "apply" { println!("parsing apply"); - let expression = super::Expression::::try_from_xml(&mut xml); + let expression = Expression::::try_from_xml(&mut xml); println!("parsed apply {:?}", expression); } } @@ -173,7 +176,7 @@ mod tests { indent += 1; if name.local_name == "transition" { println!("parsing transition"); - let update_fn = super::UpdateFn::::try_from_xml(&mut xml); + let update_fn = UpdateFn::::try_from_xml(&mut xml); println!("update fn: {:?}", update_fn); return; } diff --git a/src/prototype/expression.rs b/src/prototype/expression.rs index 84ec497..6e0b1b9 100644 --- a/src/prototype/expression.rs +++ b/src/prototype/expression.rs @@ -2,7 +2,7 @@ use std::{fmt::Debug, io::BufRead, str::FromStr}; use thiserror::Error; use xml::reader::XmlEvent; -use crate::{expect_closure_of, expect_opening, expect_opening_of, XmlReader}; +use super::{expect_closure_of, expect_opening, expect_opening_of, XmlReader}; #[derive(Debug)] pub enum Expression { diff --git a/src/prototype/mod.rs b/src/prototype/mod.rs index 4af48bd..485bfb6 100644 --- a/src/prototype/mod.rs +++ b/src/prototype/mod.rs @@ -1,3 +1,5 @@ +// todo those should likely also not be publicly exported in the final library + mod expression; pub use expression::*; @@ -23,4 +25,4 @@ mod symbolic_transition_fn; pub use symbolic_transition_fn::*; mod reachability; -pub use reachability::*; \ No newline at end of file +pub use reachability::*; diff --git a/src/prototype/reachability.rs b/src/prototype/reachability.rs index 6ff7daf..a4e24c7 100644 --- a/src/prototype/reachability.rs +++ b/src/prototype/reachability.rs @@ -1,27 +1,37 @@ -use std::fmt::Debug; use biodivine_lib_bdd::Bdd; -use crate::{count_states, log_percent, pick_state_bdd, SmartSystemUpdateFn, SymbolicDomain}; +use std::fmt::Debug; + +use crate::{ + prototype::{count_states, find_start_of, log_percent, pick_state_bdd, SmartSystemUpdateFn}, + SymbolicDomain, +}; pub fn reachability_benchmark + Debug>(sbml_path: &str) { let smart_system_update_fn = { - let file = std::fs::File::open(sbml_path.clone()) - .expect("Cannot open SBML file."); + let file = std::fs::File::open(sbml_path.clone()).expect("Cannot open SBML file."); let reader = std::io::BufReader::new(file); let mut xml = xml::reader::EventReader::new(reader); - crate::find_start_of(&mut xml, "listOfTransitions") + find_start_of(&mut xml, "listOfTransitions") .expect("Cannot find transitions in the SBML file."); let smart_system_update_fn = SmartSystemUpdateFn::::try_from_xml(&mut xml) - .expect("Loading system fn update failed."); + .expect("Loading system fn update failed."); smart_system_update_fn }; let unit = smart_system_update_fn.unit_vertex_set(); let system_var_count = smart_system_update_fn.get_system_variables().len(); - println!("Variables: {}, expected states {}", system_var_count, 1 << system_var_count); - println!("Computed state count: {}", count_states(&smart_system_update_fn, &unit)); + println!( + "Variables: {}, expected states {}", + system_var_count, + 1 << system_var_count + ); + println!( + "Computed state count: {}", + count_states(&smart_system_update_fn, &unit) + ); let mut universe = unit.clone(); while !universe.is_false() { let mut weak_scc = pick_state_bdd(&smart_system_update_fn, &universe); @@ -31,13 +41,21 @@ pub fn reachability_benchmark + Debug>(sbml_path: &str) { // FWD/BWD reachable set is not a subset of weak SCC, meaning the SCC can be expanded. if !fwd_bwd_reachable.imp(&weak_scc).is_true() { - println!(" + SCC increased to (states={}, size={})", count_states(&smart_system_update_fn, &weak_scc), weak_scc.size()); + println!( + " + SCC increased to (states={}, size={})", + count_states(&smart_system_update_fn, &weak_scc), + weak_scc.size() + ); weak_scc = fwd_bwd_reachable; } else { break; } } - println!(" + Found weak SCC (states={}, size={})", count_states(&smart_system_update_fn, &weak_scc), weak_scc.size()); + println!( + " + Found weak SCC (states={}, size={})", + count_states(&smart_system_update_fn, &weak_scc), + weak_scc.size() + ); // Remove the SCC from the universe set and start over. universe = universe.and_not(&weak_scc); println!( @@ -52,12 +70,20 @@ pub fn reachability_benchmark + Debug>(sbml_path: &str) { /// /// The result BDD contains a vertex `x` if and only if there is a (possibly zero-length) path /// from some vertex `x' \in initial` into `x`, i.e. `x' -> x`. -pub fn reach_fwd + Debug>(system: &SmartSystemUpdateFn, initial: &Bdd, universe: &Bdd) -> Bdd { +pub fn reach_fwd + Debug>( + system: &SmartSystemUpdateFn, + initial: &Bdd, + universe: &Bdd, +) -> Bdd { // The list of system variables, sorted in descending order (i.e. opposite order compared // to the ordering inside BDDs). let sorted_variables = system.get_system_variables(); let mut result = initial.clone(); - println!("Start forward reachability: (states={}, size={})", count_states(system, &result), result.size()); + println!( + "Start forward reachability: (states={}, size={})", + count_states(system, &result), + result.size() + ); 'fwd: loop { for var in sorted_variables.iter().rev() { let successors = system.transition_under_variable(var.as_str(), &result); @@ -76,7 +102,11 @@ pub fn reach_fwd + Debug>(system: &SmartSystemUpdateFn> Done. (states={}, size={})", count_states(system, &result), result.size()); + println!( + " >> Done. (states={}, size={})", + count_states(system, &result), + result.size() + ); return result; } } @@ -85,10 +115,18 @@ pub fn reach_fwd + Debug>(system: &SmartSystemUpdateFn x'`. -pub fn reach_bwd + Debug>(system: &SmartSystemUpdateFn, initial: &Bdd, universe: &Bdd) -> Bdd { +pub fn reach_bwd + Debug>( + system: &SmartSystemUpdateFn, + initial: &Bdd, + universe: &Bdd, +) -> Bdd { let sorted_variables = system.get_system_variables(); let mut result = initial.clone(); - println!("Start backward reachability: (states={}, size={})", count_states(system, &result), result.size()); + println!( + "Start backward reachability: (states={}, size={})", + count_states(system, &result), + result.size() + ); 'bwd: loop { for var in sorted_variables.iter().rev() { let predecessors = system.predecessors_under_variable(var.as_str(), &result); @@ -107,7 +145,11 @@ pub fn reach_bwd + Debug>(system: &SmartSystemUpdateFn> Done. (states={}, size={})", count_states(system, &result), result.size()); + println!( + " >> Done. (states={}, size={})", + count_states(system, &result), + result.size() + ); return result; } } diff --git a/src/prototype/smart_system_update_fn.rs b/src/prototype/smart_system_update_fn.rs index bae9f85..a731f9c 100644 --- a/src/prototype/smart_system_update_fn.rs +++ b/src/prototype/smart_system_update_fn.rs @@ -2,17 +2,25 @@ // todo how to work with the "variables" that are not mentioned in the listOfTransitions? -use std::{collections::HashMap, fmt::Debug, io::BufRead}; use std::collections::HashSet; +use std::{collections::HashMap, fmt::Debug, io::BufRead}; -use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable, BddVariableSet, BddVariableSetBuilder}; +use biodivine_lib_bdd::{ + Bdd, BddPartialValuation, BddVariable, BddVariableSet, BddVariableSetBuilder, +}; use debug_ignore::DebugIgnore; -use crate::{ - SymbolicDomain, SymbolicTransitionFn, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, - XmlReader, +use crate::SymbolicDomain; + +use super::{ + process_list, SymbolicTransitionFn, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, XmlReader, }; +// use crate::{ +// SymbolicDomain, SymbolicTransitionFn, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, +// XmlReader, +// }; + #[derive(Debug)] pub struct SmartSystemUpdateFn, T> { pub update_fns: HashMap>, @@ -437,9 +445,7 @@ impl + Debug> SmartSystemUpdateFn { /// The list of system variables, sorted in ascending order (i.e. the order in which they /// also appear within the BDDs). pub fn get_system_variables(&self) -> Vec { - let mut variables = self.update_fns.keys() - .cloned() - .collect::>(); + let mut variables = self.update_fns.keys().cloned().collect::>(); variables.sort(); variables } @@ -489,17 +495,17 @@ fn load_all_update_fns, BR: BufRead>( xml: &mut XR, // todo generic ) -> Result>, Box> { - let mut function_map: HashMap> = crate::process_list( + let mut function_map: HashMap> = process_list( "listOfTransitions", "transition", |xml, _unused_opening_tag| UpdateFn::::try_from_xml(xml), xml, )? - // todo this might not be the smartest nor useful; the name is already in the fn - // but this will allow us to access the appropriate fn quickly - .into_iter() - .map(|upd_fn| (upd_fn.target_var_name.clone(), upd_fn)) - .collect(); + // todo this might not be the smartest nor useful; the name is already in the fn + // but this will allow us to access the appropriate fn quickly + .into_iter() + .map(|upd_fn| (upd_fn.target_var_name.clone(), upd_fn)) + .collect(); let input_names: HashSet = function_map .values() @@ -510,12 +516,7 @@ fn load_all_update_fns, BR: BufRead>( if !function_map.contains_key(&name) { // This variable is an input. For now, we just fix all inputs to `false`. // TODO: We need to handle inputs properly in the future, but not today. - let update = UpdateFn::new( - Vec::new(), - name.clone(), - Vec::new(), - 0u8 - ); + let update = UpdateFn::new(Vec::new(), name.clone(), Vec::new(), 0u8); function_map.insert(name, update); } } @@ -642,26 +643,15 @@ fn get_max_val_of_var_in_all_transitions_including_their_own( #[cfg(test)] mod tests { + use std::{collections::HashMap, ops::Add, sync::RwLock}; + use biodivine_lib_bdd::BddVariableSetBuilder; use rayon::prelude::{IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator}; - use xml::EventReader; use crate::{ - prototype::smart_system_update_fn::{self, SmartSystemUpdateFn}, - symbolic_domain::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain}, - SymbolicDomain, SystemUpdateFn, UnaryIntegerDomain, XmlReader, - }; - - // use std:io::{BufRead, BufReader} - - use core::panic; - use std::{ - cell::RefCell, - io::BufReader, - ops::Add, - sync::{Arc, RwLock}, + prototype::{find_start_of, SmartSystemUpdateFn, SystemUpdateFn}, + BinaryIntegerDomain, UnaryIntegerDomain, }; - use std::{collections::HashMap, io::BufRead}; // use super::SystemUpdateFn; @@ -707,7 +697,7 @@ mod tests { std::fs::File::open(dirent.path()).unwrap(), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn, u8> = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -748,7 +738,7 @@ mod tests { std::fs::File::open(dirent.path()).unwrap(), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn, u8> = SystemUpdateFn::try_from_xml(&mut xml) @@ -815,7 +805,7 @@ mod tests { .expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -862,7 +852,7 @@ mod tests { println!("---force"); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -916,7 +906,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -930,7 +920,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -990,7 +980,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn, u8> = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1004,7 +994,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn, u8> = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -1078,7 +1068,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1092,7 +1082,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -1253,7 +1243,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn, u8> = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1267,7 +1257,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn, u8> = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -1386,7 +1376,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn, u8> = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1400,7 +1390,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn, u8> = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -1480,7 +1470,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1494,7 +1484,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml) @@ -1635,7 +1625,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1649,7 +1639,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml) @@ -1825,7 +1815,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -1839,7 +1829,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); @@ -2242,7 +2232,7 @@ mod tests { std::fs::File::open(filepath.clone()).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let smart_system_update_fn: SmartSystemUpdateFn = SmartSystemUpdateFn::try_from_xml(&mut xml) @@ -2256,7 +2246,7 @@ mod tests { std::fs::File::open(filepath).expect("cannot open the file"), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find list"); let force_system_update_fn: SystemUpdateFn = SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn"); diff --git a/src/prototype/symbolic_transition_fn.rs b/src/prototype/symbolic_transition_fn.rs index 461d8bb..5b99260 100644 --- a/src/prototype/symbolic_transition_fn.rs +++ b/src/prototype/symbolic_transition_fn.rs @@ -2,7 +2,11 @@ use std::fmt::Debug; use biodivine_lib_bdd::{Bdd, BddVariableSet}; -use crate::{SymbolicDomain, VariableUpdateFnCompiled}; +use crate::SymbolicDomain; + +use super::VariableUpdateFnCompiled; + +// use crate::{SymbolicDomain, VariableUpdateFnCompiled}; #[derive(Debug)] pub struct SymbolicTransitionFn, T> { diff --git a/src/prototype/system_update_fn.rs b/src/prototype/system_update_fn.rs index ce97495..92b1137 100644 --- a/src/prototype/system_update_fn.rs +++ b/src/prototype/system_update_fn.rs @@ -9,7 +9,11 @@ use biodivine_lib_bdd::{ }; use debug_ignore::DebugIgnore; -use crate::{SymbolicDomain, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, XmlReader}; +use crate::SymbolicDomain; + +use super::{process_list, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, XmlReader}; + +// use crate::{SymbolicDomain, UpdateFn, UpdateFnBdd, VariableUpdateFnCompiled, XmlReader}; #[derive(Debug)] pub struct SystemUpdateFn, T> { @@ -656,7 +660,7 @@ fn load_all_update_fns, BR: BufRead>( xml: &mut XR, // todo generic ) -> Result>, Box> { - Ok(crate::process_list( + Ok(process_list( "listOfTransitions", "transition", |xml, _unused_opening_tag| UpdateFn::::try_from_xml(xml), @@ -788,15 +792,20 @@ fn get_max_val_of_var_in_all_transitions_including_their_own_and_detect_where_co #[cfg(test)] mod tests { - use crate::{ - symbolic_domain::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain}, - SymbolicDomain, UnaryIntegerDomain, XmlReader, - }; + // use crate::{ + // symbolic_domain::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain}, + // SymbolicDomain, UnaryIntegerDomain, XmlReader, + // }; // use std:io::{BufRead, BufReader} - use std::io::BufRead; - use std::io::BufReader; + // use std::io::BufRead; + // use std::io::BufReader; + + use crate::{ + prototype::{find_start_of, CountingReader, DebuggingReader, LoudReader, XmlReader}, + BinaryIntegerDomain, SymbolicDomain, UnaryIntegerDomain, + }; use super::SystemUpdateFn; @@ -806,9 +815,9 @@ mod tests { let br = std::io::BufReader::new(file); let reader = xml::reader::EventReader::new(br); - let mut reader = crate::LoudReader::new(reader); // uncomment to see how xml is loaded + let mut reader = LoudReader::new(reader); // uncomment to see how xml is loaded - crate::find_start_of(&mut reader, "listOfTransitions").expect("cannot find start of list"); + find_start_of(&mut reader, "listOfTransitions").expect("cannot find start of list"); let system_update_fn: SystemUpdateFn = super::SystemUpdateFn::try_from_xml(&mut reader).unwrap(); @@ -828,7 +837,7 @@ mod tests { std::fs::File::open("data/bigger.sbml").unwrap(), )); - crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find start of list"); + find_start_of(&mut xml, "listOfTransitions").expect("cannot find start of list"); let system_update_fn: SystemUpdateFn, u8> = super::SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load system update fn"); @@ -855,10 +864,9 @@ mod tests { std::fs::File::open(dirent.path()).unwrap(), )); - let mut counting = crate::CountingReader::new(xml); + let mut counting = CountingReader::new(xml); - crate::find_start_of(&mut counting, "listOfTransitions") - .expect("could not find list"); + find_start_of(&mut counting, "listOfTransitions").expect("could not find list"); let start = counting.curr_line; @@ -888,10 +896,9 @@ mod tests { std::fs::File::open(dirent.path()).unwrap(), )); - let mut counting = crate::CountingReader::new(xml); + let mut counting = CountingReader::new(xml); - crate::find_start_of(&mut counting, "listOfTransitions") - .expect("could not find list"); + find_start_of(&mut counting, "listOfTransitions").expect("could not find list"); let all_update_fns = super::load_all_update_fns(&mut counting) .expect("could not even load the damn thing"); @@ -899,7 +906,7 @@ mod tests { let xml = xml::reader::EventReader::new(std::io::BufReader::new( std::fs::File::open(dirent.path()).unwrap(), )); - let mut debug_xml = crate::DebuggingReader::new(xml, &all_update_fns, true, true); + let mut debug_xml = DebuggingReader::new(xml, &all_update_fns, true, true); // while let Ok(_) = debug_xml.next() {} @@ -929,7 +936,7 @@ mod tests { std::fs::File::open("data/update_fn_test.sbml").unwrap(), )); - crate::find_start_of(&mut reader, "listOfTransitions").expect("cannot find start of list"); + find_start_of(&mut reader, "listOfTransitions").expect("cannot find start of list"); let system_update_fn: SystemUpdateFn = super::SystemUpdateFn::try_from_xml(&mut reader).unwrap(); diff --git a/src/prototype/update_fn.rs b/src/prototype/update_fn.rs index 5ab54d1..02a3a72 100644 --- a/src/prototype/update_fn.rs +++ b/src/prototype/update_fn.rs @@ -1,7 +1,6 @@ -use crate::{expect_closure_of, expect_opening_of, process_list, StartElementWrapper, XmlReader}; - -use super::expression::Expression; use super::utils::expect_opening; +use super::{expect_closure_of, expect_opening_of, process_list, StartElementWrapper}; +use super::{expression::Expression, XmlReader}; use std::{io::BufRead, str::FromStr}; /// represents collection of tuples of the result values and the associated conditions. there is also the default value. diff --git a/src/prototype/update_fn_bdd.rs b/src/prototype/update_fn_bdd.rs index 563b83e..1fb0719 100644 --- a/src/prototype/update_fn_bdd.rs +++ b/src/prototype/update_fn_bdd.rs @@ -1,12 +1,12 @@ use std::{collections::HashMap, fmt::Debug}; -use biodivine_lib_bdd::{ - Bdd, BddPartialValuation, BddValuation, BddVariableSet, -}; +use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddValuation, BddVariableSet}; -use crate::{Expression, SymbolicDomain, UpdateFn}; +// use crate::{Expression, SymbolicDomain, UpdateFn}; -use super::expression::Proposition; +use crate::SymbolicDomain; + +use super::{expression::Proposition, Expression, UpdateFn}; // todo this should be abstacted into a geeneric parameter // todo but that would require diff --git a/src/prototype/update_fn_compiled.rs b/src/prototype/update_fn_compiled.rs index a83df2e..365b908 100644 --- a/src/prototype/update_fn_compiled.rs +++ b/src/prototype/update_fn_compiled.rs @@ -1,10 +1,12 @@ use std::collections::HashMap; -use biodivine_lib_bdd::{ - Bdd, BddPartialValuation, BddValuation, BddVariable, -}; +use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddValuation, BddVariable}; -use crate::{SymbolicDomain, UpdateFnBdd}; +use crate::SymbolicDomain; + +use super::UpdateFnBdd; + +// use crate::{SymbolicDomain, UpdateFnBdd}; // type ValueType = u8; @@ -143,12 +145,7 @@ impl, T> VariableUpdateFnCompiled { mod tests { use biodivine_lib_bdd::{BddPartialValuation, BddVariableSetBuilder}; - use crate::{ - get_test_update_fn, - prototype::update_fn_compiled::VariableUpdateFnCompiled, - symbolic_domain::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain}, - SymbolicDomain, UnaryIntegerDomain, UpdateFnBdd, - }; + use crate::SymbolicDomain; #[derive(Clone)] struct FakeDomain; diff --git a/src/prototype/utils.rs b/src/prototype/utils.rs index 96d9605..ba10cd2 100644 --- a/src/prototype/utils.rs +++ b/src/prototype/utils.rs @@ -1,8 +1,8 @@ use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable}; -use std::{collections::HashMap, io::BufRead, str::FromStr}; +use num_bigint::BigInt; use std::fmt::Debug; use std::ops::Shr; -use num_bigint::BigInt; +use std::{collections::HashMap, io::BufRead, str::FromStr}; use xml::{ attribute::OwnedAttribute, name::OwnedName, @@ -10,7 +10,11 @@ use xml::{ reader::{EventReader, XmlEvent}, }; -use crate::{SmartSystemUpdateFn, SymbolicDomain, UpdateFn}; +use crate::SymbolicDomain; + +use super::{SmartSystemUpdateFn, UpdateFn}; + +// use crate::{SmartSystemUpdateFn, SymbolicDomain, UpdateFn}; pub fn expect_opening, BR: BufRead>( xml: &mut XR, @@ -463,27 +467,33 @@ pub fn find_bdd_variables_prime, T>( }) } - /// Compute a [Bdd] which represents a single (un-primed) state within the given symbolic `set`. -pub fn pick_state_bdd + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> Bdd { +pub fn pick_state_bdd + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> Bdd { // Unfortunately, this is now a bit more complicated than it needs to be, because // we have to ignore the primed variables, but it shouldn't bottleneck anything outside of // truly extreme cases. let standard_variables = system.standard_variables(); - let valuation = set.sat_witness() + let valuation = set + .sat_witness() .expect("Cannot pick state from an empty set."); let mut state_data = BddPartialValuation::empty(); for var in standard_variables { state_data.set_value(var, valuation.value(var)) } - system.get_bdd_variable_set().mk_conjunctive_clause(&state_data) + system + .get_bdd_variable_set() + .mk_conjunctive_clause(&state_data) } - /// Pick a state from a symbolic set and "decode" it into normal integers. -pub fn pick_state_map + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> HashMap { - let valuation = set.sat_witness() - .expect("The set is empty."); +pub fn pick_state_map + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> HashMap { + let valuation = set.sat_witness().expect("The set is empty."); let valuation = BddPartialValuation::from(valuation); let mut result = HashMap::new(); for var in system.get_system_variables() { @@ -498,8 +508,11 @@ pub fn pick_state_map + Debug>(system: &SmartSystemUpdateF /// Encode a "state" (assignment of integer values to all variables) into a [Bdd] that is valid /// within the provided [SmartSystemUpdateFn]. -pub fn encode_state_map + Debug>(system: &SmartSystemUpdateFn, state: &HashMap) -> Bdd { - let mut result = BddPartialValuation::empty(); +pub fn encode_state_map + Debug>( + system: &SmartSystemUpdateFn, + state: &HashMap, +) -> Bdd { + let mut result = BddPartialValuation::empty(); for var in system.get_system_variables() { let Some(value) = state.get(&var) else { panic!("Value for {var} missing."); @@ -517,7 +530,10 @@ pub fn log_percent(set: &Bdd, universe: &Bdd) -> f64 { } /// Compute an (approximate) count of state in the given `set` using the encoding of `system`. -pub fn count_states + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> f64 { +pub fn count_states + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> f64 { let symbolic_var_count = system.get_bdd_variable_set().num_vars() as i32; // TODO: // Here we assume that exactly half of the variables are primed, which may not be true @@ -528,7 +544,10 @@ pub fn count_states + Debug>(system: &SmartSystemUpdateFn< } /// Same as [count_states], but with exact unbounded integers. -pub fn count_states_exact + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> BigInt { +pub fn count_states_exact + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> BigInt { let symbolic_var_count = system.get_bdd_variable_set().num_vars() as i32; // TODO: // Here we assume that exactly half of the variables are primed, which may not be true @@ -536,4 +555,4 @@ pub fn count_states_exact + Debug>(system: &SmartSystemUpd assert_eq!(symbolic_var_count % 2, 0); let primed_vars = symbolic_var_count / 2; set.exact_cardinality().shr(primed_vars) -} \ No newline at end of file +} diff --git a/src/test_utils.rs b/src/test_utils.rs index 3da4287..884a723 100644 --- a/src/test_utils.rs +++ b/src/test_utils.rs @@ -1,7 +1,15 @@ -use std::fmt::Debug; use biodivine_lib_bdd::Bdd; use num_bigint::BigInt; -use crate::{BinaryIntegerDomain, count_states_exact, encode_state_map, find_start_of, GrayCodeIntegerDomain, PetriNetIntegerDomain, pick_state_map, SmartSystemUpdateFn, SymbolicDomain, UnaryIntegerDomain}; +use std::fmt::Debug; + +use crate::{ + prototype::{ + count_states_exact, encode_state_map, find_start_of, pick_state_map, SmartSystemUpdateFn, + }, + BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, SymbolicDomain, + UnaryIntegerDomain, +}; +// use crate::{BinaryIntegerDomain, count_states_exact, encode_state_map, find_start_of, GrayCodeIntegerDomain, PetriNetIntegerDomain, pick_state_map, SmartSystemUpdateFn, SymbolicDomain, UnaryIntegerDomain}; pub struct ComputationStep { steps: usize, @@ -21,7 +29,10 @@ pub struct ComputationStep { /// Perform one step of backward reachability procedure. Returns either a new [Bdd] value, or /// `None` if no new predecessors can be included. -fn bwd_step + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> Option { +fn bwd_step + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> Option { let sorted_variables = system.get_system_variables(); for var in sorted_variables.iter().rev() { @@ -38,7 +49,10 @@ fn bwd_step + Debug>(system: &SmartSystemUpdateFn, } /// The same as [bwd_step], but goes forwards, not backward. -fn fwd_step + Debug>(system: &SmartSystemUpdateFn, set: &Bdd) -> Option { +fn fwd_step + Debug>( + system: &SmartSystemUpdateFn, + set: &Bdd, +) -> Option { let sorted_variables = system.get_system_variables(); for var in sorted_variables.iter().rev() { @@ -56,8 +70,7 @@ fn fwd_step + Debug>(system: &SmartSystemUpdateFn, /// A generic function that builds [SmartSystemUpdateFn] from an SBML file. fn build_update_fn + Debug>(sbml_path: &str) -> SmartSystemUpdateFn { - let file = std::fs::File::open(sbml_path.clone()) - .expect("Cannot open SBML file."); + let file = std::fs::File::open(sbml_path.clone()).expect("Cannot open SBML file."); let reader = std::io::BufReader::new(file); let mut xml = xml::reader::EventReader::new(reader); @@ -71,7 +84,6 @@ fn build_update_fn + Debug>(sbml_path: &str) -> SmartSyste } impl ComputationStep { - pub fn new(sbml_path: &str) -> ComputationStep { let system_unary = build_update_fn::(sbml_path); let system_binary = build_update_fn::>(sbml_path); @@ -126,7 +138,10 @@ impl ComputationStep { self.result_unary = bwd_step(&self.system_unary, self.result_unary.as_ref().unwrap()); self.result_binary = bwd_step(&self.system_binary, self.result_binary.as_ref().unwrap()); self.result_gray = bwd_step(&self.system_gray, self.result_gray.as_ref().unwrap()); - self.result_petri_net = bwd_step(&self.system_petri_net, self.result_petri_net.as_ref().unwrap()); + self.result_petri_net = bwd_step( + &self.system_petri_net, + self.result_petri_net.as_ref().unwrap(), + ); if let Some(result_unary) = &self.result_unary { self.universe_unary = self.universe_unary.and_not(result_unary); } @@ -146,7 +161,10 @@ impl ComputationStep { self.result_unary = fwd_step(&self.system_unary, self.result_unary.as_ref().unwrap()); self.result_binary = fwd_step(&self.system_binary, self.result_binary.as_ref().unwrap()); self.result_gray = fwd_step(&self.system_gray, self.result_gray.as_ref().unwrap()); - self.result_petri_net = fwd_step(&self.system_petri_net, self.result_petri_net.as_ref().unwrap()); + self.result_petri_net = fwd_step( + &self.system_petri_net, + self.result_petri_net.as_ref().unwrap(), + ); if let Some(result_unary) = &self.result_unary { self.universe_unary = self.universe_unary.and_not(result_unary); } @@ -162,29 +180,35 @@ impl ComputationStep { } pub fn check_consistency(&self) { - let count_unary = self.result_unary.as_ref().map(|it| { - count_states_exact(&self.system_unary, &it) - }); - let count_binary = self.result_binary.as_ref().map(|it| { - count_states_exact(&self.system_binary, &it) - }); - let count_gray = self.result_gray.as_ref().map(|it| { - count_states_exact(&self.system_gray, &it) - }); - let count_petri_net = self.result_petri_net.as_ref().map(|it| { - count_states_exact(&self.system_petri_net, &it) - }); - if count_unary != count_binary || count_binary != count_gray || count_gray != count_petri_net { + let count_unary = self + .result_unary + .as_ref() + .map(|it| count_states_exact(&self.system_unary, &it)); + let count_binary = self + .result_binary + .as_ref() + .map(|it| count_states_exact(&self.system_binary, &it)); + let count_gray = self + .result_gray + .as_ref() + .map(|it| count_states_exact(&self.system_gray, &it)); + let count_petri_net = self + .result_petri_net + .as_ref() + .map(|it| count_states_exact(&self.system_petri_net, &it)); + if count_unary != count_binary + || count_binary != count_gray + || count_gray != count_petri_net + { panic!( "Error at step {}. {:?} <> {:?} <> {:?} <> {:?}", - self.steps, - count_unary, - count_binary, - count_gray, - count_petri_net + self.steps, count_unary, count_binary, count_gray, count_petri_net ) } else { - println!("Step {} successful. Current result state count: {:?}", self.steps, count_unary); + println!( + "Step {} successful. Current result state count: {:?}", + self.steps, count_unary + ); println!( " > BDD sizes: {:?} {:?} {:?} {:?}", self.result_unary.as_ref().map(|it| it.size()), @@ -194,5 +218,4 @@ impl ComputationStep { ); } } - -} \ No newline at end of file +}