refactor: fixed the problem with the public exporting

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::<Vec<_>>();
@@ -12,4 +15,4 @@ fn main() {
         "gray" | "grey" => reachability_benchmark::<GrayCodeIntegerDomain<u8>>(sbml_path.as_str()),
         _ => panic!("Unknown representation: {}.", representation),
     }
-}
+}

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::<u8>::try_from_xml(&mut xml);
+                        let expression = Expression::<u8>::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::<u8>::try_from_xml(&mut xml);
+                        let update_fn = UpdateFn::<u8>::try_from_xml(&mut xml);
                         println!("update fn: {:?}", update_fn);
                         return;
                     }

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<T> {

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::*;
+pub use reachability::*;

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<D: SymbolicDomain<u8> + 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::<D, u8>::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<D: SymbolicDomain<u8> + 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<D: SymbolicDomain<u8> + 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<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D, u8>, initial: &Bdd, universe: &Bdd) -> Bdd {
+pub fn reach_fwd<D: SymbolicDomain<u8> + Debug>(
+    system: &SmartSystemUpdateFn<D, u8>,
+    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<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
         }
 
         // No further successors were computed across all variables. We are done.
-        println!(" >> 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<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
 ///
 /// The result BDD contains a vertex `x` if and only if there is a (possibly zero-length) path
 /// from `x` into some vertex `x' \in initial`, i.e. `x -> x'`.
-pub fn reach_bwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D, u8>, initial: &Bdd, universe: &Bdd) -> Bdd {
+pub fn reach_bwd<D: SymbolicDomain<u8> + Debug>(
+    system: &SmartSystemUpdateFn<D, u8>,
+    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<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
         }
 
         // No further predecessors were computed across all variables. We are done.
-        println!(" >> Done. (states={}, size={})", count_states(system, &result), result.size());
+        println!(
+            " >> Done. (states={}, size={})",
+            count_states(system, &result),
+            result.size()
+        );
         return result;
     }
 }