Merge branch 'master' into 0.5.0

src/bin/bench_reach_symbolic.rs

@@ -0,0 +1,39 @@
+use biodivine_lib_param_bn::biodivine_std::traits::Set;
+use biodivine_lib_param_bn::symbolic_async_graph::reachability::Reachability;
+use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
+use biodivine_lib_param_bn::BooleanNetwork;
+
+fn main() {
+    let args = Vec::from_iter(std::env::args());
+    let path = &args[1];
+    let model = BooleanNetwork::try_from_file(path).unwrap();
+    let model = model.inline_inputs(true, true);
+
+    println!(
+        "Loaded model with {} variables and {} parameters.",
+        model.num_vars(),
+        model.num_parameters()
+    );
+
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
+
+    let mut count = 0;
+    let mut universe = stg.mk_unit_colored_vertices();
+    while !universe.is_empty() {
+        let reduced_stg = stg.restrict(&universe);
+        let mut component = universe.pick_vertex();
+        loop {
+            let update = Reachability::reach_bwd(&reduced_stg, &component);
+            let update = Reachability::reach_fwd(&reduced_stg, &update);
+            if update.is_subset(&component) {
+                break;
+            } else {
+                component = update;
+            }
+        }
+        println!("Found weak component: {}", component.approx_cardinality());
+        universe = universe.minus(&component);
+        count += 1;
+    }
+    println!("Total {count} components.")
+}

src/bin/bench_reach_symbolic_basic.rs

@@ -0,0 +1,39 @@
+use biodivine_lib_param_bn::biodivine_std::traits::Set;
+use biodivine_lib_param_bn::symbolic_async_graph::reachability::Reachability;
+use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
+use biodivine_lib_param_bn::BooleanNetwork;
+
+fn main() {
+    let args = Vec::from_iter(std::env::args());
+    let path = &args[1];
+    let model = BooleanNetwork::try_from_file(path).unwrap();
+    let model = model.inline_inputs(true, true);
+
+    println!(
+        "Loaded model with {} variables and {} parameters.",
+        model.num_vars(),
+        model.num_parameters()
+    );
+
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
+
+    let mut count = 0;
+    let mut universe = stg.mk_unit_colored_vertices();
+    while !universe.is_empty() {
+        let reduced_stg = stg.restrict(&universe);
+        let mut component = universe.pick_vertex();
+        loop {
+            let update = Reachability::reach_bwd_basic(&reduced_stg, &component);
+            let update = Reachability::reach_fwd_basic(&reduced_stg, &update);
+            if update.is_subset(&component) {
+                break;
+            } else {
+                component = update;
+            }
+        }
+        println!("Found weak component: {}", component.approx_cardinality());
+        universe = universe.minus(&component);
+        count += 1;
+    }
+    println!("Total {count} components.")
+}

src/symbolic_async_graph/_impl_function_table.rs

@@ -14,7 +14,8 @@ impl FunctionTable {
                 bdd_builder.make_variable(bdd_var_name.as_str())
             })
             .collect();
-        FunctionTable { arity, rows }
+        let name = name.to_string();
+        FunctionTable { arity, rows, name }
     }
 
     /// List the symbolic variables that appear in this function table.
@@ -25,6 +26,11 @@ impl FunctionTable {
     pub fn symbolic_variables(&self) -> &Vec<BddVariable> {
         &self.rows
     }
+
+    /// True if this [FunctionTable] contains the provided [BddVariable].
+    pub fn contains(&self, var: BddVariable) -> bool {
+        self.rows.contains(&var)
+    }
 }
 
 /// Converts a `FunctionTable` into an iterator of `Vec<bool>` (function table row) and

src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs

@@ -1,4 +1,5 @@
 use crate::biodivine_std::traits::Set;
+use crate::symbolic_async_graph::reachability::Reachability;
 use crate::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use crate::{ExtendedBoolean, Space, VariableId};
 
@@ -13,36 +14,14 @@ impl SymbolicAsyncGraph {
     ///
     /// In other words, the result is the smallest forward-closed superset of `initial`.
     pub fn reach_forward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
-        let mut result = initial.clone();
-        'fwd: loop {
-            for var in self.variables().rev() {
-                let step = self.var_post_out(var, &result);
-                if !step.is_empty() {
-                    result = result.union(&step);
-                    continue 'fwd;
-                }
-            }
-
-            return result;
-        }
+        Reachability::reach_fwd(self, initial)
     }
 
     /// Compute the set of backward-reachable vertices from the given `initial` set.
     ///
     /// In other words, the result is the smallest backward-closed superset of `initial`.
     pub fn reach_backward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
-        let mut result = initial.clone();
-        'bwd: loop {
-            for var in self.variables().rev() {
-                let step = self.var_pre_out(var, &result);
-                if !step.is_empty() {
-                    result = result.union(&step);
-                    continue 'bwd;
-                }
-            }
-
-            return result;
-        }
+        Reachability::reach_bwd(self, initial)
     }
 
     /// Compute the subset of `initial` vertices that can only reach other vertices within
@@ -139,6 +118,7 @@ impl SymbolicAsyncGraph {
 #[cfg(test)]
 mod tests {
     use crate::biodivine_std::traits::Set;
+    use crate::symbolic_async_graph::reachability::Reachability;
     use crate::symbolic_async_graph::SymbolicAsyncGraph;
     use crate::ExtendedBoolean::Zero;
     use crate::{BooleanNetwork, ExtendedBoolean, Space};
@@ -165,6 +145,8 @@ mod tests {
         let pivot = stg.unit_colored_vertices().pick_vertex();
         let fwd = stg.reach_forward(&pivot);
         let bwd = stg.reach_backward(&pivot);
+        let fwd_basic = Reachability::reach_fwd_basic(&stg, &pivot);
+        let bwd_basic = Reachability::reach_bwd_basic(&stg, &pivot);
         let scc = fwd.intersect(&bwd);
 
         // Should contain all cases where pivot is in an attractor.
@@ -179,6 +161,13 @@ mod tests {
         // For some reason, there is only a very small number of parameter valuations
         // where this is not empty -- less than in the pivot in fact.
         assert!(!repeller_basin.is_empty());
+
+        assert!(pivot.is_subset(&fwd));
+        assert!(pivot.is_subset(&bwd));
+        assert!(pivot.is_subset(&scc));
+
+        assert_eq!(fwd, fwd_basic);
+        assert_eq!(bwd, bwd_basic);
     }
 
     #[test]