From e3f3927926505daad56538304c2c3650d56db441 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Tue, 28 Feb 2023 23:07:37 +0100 Subject: [PATCH 1/5] Proposal for new, faster reachability procedures. --- src/bin/bench_reach_symbolic.rs | 39 +++++ src/bin/bench_reach_symbolic_basic.rs | 39 +++++ .../_impl_symbolic_async_graph.rs | 11 +- src/symbolic_async_graph/mod.rs | 2 + src/symbolic_async_graph/reachability.rs | 159 ++++++++++++++++++ 5 files changed, 249 insertions(+), 1 deletion(-) create mode 100644 src/bin/bench_reach_symbolic.rs create mode 100644 src/bin/bench_reach_symbolic_basic.rs create mode 100644 src/symbolic_async_graph/reachability.rs diff --git a/src/bin/bench_reach_symbolic.rs b/src/bin/bench_reach_symbolic.rs new file mode 100644 index 0000000..d9dcb11 --- /dev/null +++ b/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(); + + 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.") +} diff --git a/src/bin/bench_reach_symbolic_basic.rs b/src/bin/bench_reach_symbolic_basic.rs new file mode 100644 index 0000000..6f3273f --- /dev/null +++ b/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(); + + 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.") +} diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs index 83dc0a6..9b65a15 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs +++ b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs @@ -291,7 +291,7 @@ impl SymbolicAsyncGraph { symbolic_context: self.symbolic_context.clone(), vertex_space: (self.mk_empty_vertices(), set.clone()), color_space: (self.mk_empty_colors(), set.colors()), - unit_bdd: set.bdd.clone(), + unit_bdd: self.unit_bdd.and(&set.bdd), update_functions: self .update_functions .iter() @@ -637,6 +637,15 @@ impl SymbolicAsyncGraph { Ok(self.unit_colors().copy(colors)) } + + /// Obtain a reference to the underlying raw `Bdd` which evaluates + /// the variable's update function. + /// + /// Intuitively, this `Bdd` corresponds to the set of all vertex-color pairs that can perform + /// a transition under the given `variable`. This is a very low-level functionality. + pub fn raw_function_bdd(&self, variable: VariableId) -> &Bdd { + &self.update_functions[variable.to_index()] + } } #[cfg(test)] diff --git a/src/symbolic_async_graph/mod.rs b/src/symbolic_async_graph/mod.rs index 4be6b7e..bc281d2 100644 --- a/src/symbolic_async_graph/mod.rs +++ b/src/symbolic_async_graph/mod.rs @@ -59,6 +59,8 @@ mod _impl_symbolic_context; /// that are used to iterate through various projections of symbolic sets. pub mod projected_iteration; +pub mod reachability; + /// A module with a trait that describes common methods shared by all set representations /// based on BDDs. /// diff --git a/src/symbolic_async_graph/reachability.rs b/src/symbolic_async_graph/reachability.rs new file mode 100644 index 0000000..3747f73 --- /dev/null +++ b/src/symbolic_async_graph/reachability.rs @@ -0,0 +1,159 @@ +use crate::biodivine_std::traits::Set; +use crate::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; +use crate::VariableId; +use std::cmp::max; +use std::collections::HashSet; + +pub struct Reachability { + _dummy: (), +} + +impl Reachability { + pub fn reach_fwd( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + ) -> GraphColoredVertices { + Self::reach(graph, initial, |g, s, v| g.var_post_out(v, s)) + } + + pub fn reach_bwd( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + ) -> GraphColoredVertices { + Self::reach(graph, initial, |g, s, v| g.var_pre_out(v, s)) + } + + pub fn reach_fwd_basic( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + ) -> GraphColoredVertices { + Self::reach_basic_saturation(graph, initial, |g, s, v| g.var_post_out(v, s)) + } + + pub fn reach_bwd_basic( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + ) -> GraphColoredVertices { + Self::reach_basic_saturation(graph, initial, |g, s, v| g.var_pre_out(v, s)) + } + + pub fn reach_basic_saturation< + F: Fn(&SymbolicAsyncGraph, &GraphColoredVertices, VariableId) -> GraphColoredVertices, + >( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + step: F, + ) -> GraphColoredVertices { + if cfg!(feature = "print-progress") { + println!( + "Start basic symbolic reachability with {}[nodes:{}] candidates.", + initial.approx_cardinality(), + initial.symbolic_size() + ); + } + + let mut result = initial.clone(); + let network = graph.as_network(); + + let mut max_size = 0; + + 'reach: loop { + for var in network.variables().rev() { + let step = step(graph, &result, var); + if !step.is_empty() { + result = result.union(&step); + max_size = max(max_size, result.symbolic_size()); + + if cfg!(feature = "print-progress") { + let current = result.approx_cardinality(); + let max = graph.unit_colored_vertices().approx_cardinality(); + println!( + " >> Reach progress: {}[nodes:{}] candidates ({:.2} log-%).", + result.approx_cardinality(), + result.symbolic_size(), + (current.log2() / max.log2()) * 100.0 + ); + } + + continue 'reach; + } + } + + if cfg!(feature = "print-progress") { + println!( + "Basic reachability done: {}[nodes:{}] candidates. Max intermediate size: {}.", + result.approx_cardinality(), + result.symbolic_size(), + max_size + ); + } + + return result; + } + } + + /// Use [`SymbolicAsyncGraph::restrict`] to limit the reachability search to a particular + /// subgraph. + pub fn reach< + F: Fn(&SymbolicAsyncGraph, &GraphColoredVertices, VariableId) -> GraphColoredVertices, + >( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + step: F, + ) -> GraphColoredVertices { + if cfg!(feature = "print-progress") { + println!( + "Start symbolic reachability with {}[nodes:{}] candidates.", + initial.approx_cardinality(), + initial.symbolic_size() + ); + } + + let mut result = initial.clone(); + let mut max_size = 0; + let network = graph.as_network(); + let mut saturated = HashSet::new(); + 'reach: loop { + for var in network.variables().rev() { + let next_step = step(graph, &result, var); + if next_step.is_empty() { + saturated.insert(var); + } else { + result = result.union(&next_step); + max_size = max(max_size, result.symbolic_size()); + + if cfg!(feature = "print-progress") { + let current = result.approx_cardinality(); + let max = graph.unit_colored_vertices().approx_cardinality(); + println!( + " >> [{}/{} saturated] Reach progress: {}[nodes:{}] candidates ({:.2} log-%).", + saturated.len(), + network.num_vars(), + result.approx_cardinality(), + result.symbolic_size(), + (current.log2() / max.log2()) * 100.0 + ); + } + + if !saturated.contains(&var) { + for t in network.targets(var) { + saturated.remove(&t); + } + continue 'reach; + } + } + } + + if cfg!(feature = "print-progress") { + println!( + "Basic reachability done: {}[nodes:{}] candidates. Max intermediate size: {}.", + result.approx_cardinality(), + result.symbolic_size(), + max_size + ); + } + + return result; + } + } +} From 8778136a80adb89f58ca2e0eeb30c6c93ed64947 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Mon, 18 Dec 2023 15:50:05 +0100 Subject: [PATCH 2/5] Adapt to `0.5.0`. --- src/bin/bench_reach_symbolic.rs | 4 +-- src/bin/bench_reach_symbolic_basic.rs | 4 +-- src/symbolic_async_graph/reachability.rs | 33 ++++++++++++++++++------ 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/bin/bench_reach_symbolic.rs b/src/bin/bench_reach_symbolic.rs index d9dcb11..a15152d 100644 --- a/src/bin/bench_reach_symbolic.rs +++ b/src/bin/bench_reach_symbolic.rs @@ -7,7 +7,7 @@ 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(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", @@ -15,7 +15,7 @@ fn main() { model.num_parameters() ); - let stg = SymbolicAsyncGraph::new(model).unwrap(); + let stg = SymbolicAsyncGraph::new(&model).unwrap(); let mut count = 0; let mut universe = stg.mk_unit_colored_vertices(); diff --git a/src/bin/bench_reach_symbolic_basic.rs b/src/bin/bench_reach_symbolic_basic.rs index 6f3273f..6f01d96 100644 --- a/src/bin/bench_reach_symbolic_basic.rs +++ b/src/bin/bench_reach_symbolic_basic.rs @@ -7,7 +7,7 @@ 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(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", @@ -15,7 +15,7 @@ fn main() { model.num_parameters() ); - let stg = SymbolicAsyncGraph::new(model).unwrap(); + let stg = SymbolicAsyncGraph::new(&model).unwrap(); let mut count = 0; let mut universe = stg.mk_unit_colored_vertices(); diff --git a/src/symbolic_async_graph/reachability.rs b/src/symbolic_async_graph/reachability.rs index 3747f73..4bf57aa 100644 --- a/src/symbolic_async_graph/reachability.rs +++ b/src/symbolic_async_graph/reachability.rs @@ -2,7 +2,7 @@ use crate::biodivine_std::traits::Set; use crate::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; use crate::VariableId; use std::cmp::max; -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; pub struct Reachability { _dummy: (), @@ -53,12 +53,11 @@ impl Reachability { } let mut result = initial.clone(); - let network = graph.as_network(); let mut max_size = 0; 'reach: loop { - for var in network.variables().rev() { + for var in graph.variables().rev() { let step = step(graph, &result, var); if !step.is_empty() { result = result.union(&step); @@ -109,12 +108,30 @@ impl Reachability { ); } + // Construct a symbolic regulators relation (this is more accurate than the normal regulatory graph, + // and does not require an underlying Boolean network). + let targets_of_var = graph + .variables() + .map(|regulator| { + let targets = graph + .variables() + .filter(|var| { + let update = graph.get_symbolic_fn_update(*var); + let state_variable = graph.symbolic_context().get_state_variable(regulator); + update.support_set().contains(&state_variable) + }) + .collect::>(); + (regulator, targets) + }) + .collect::>(); + let mut result = initial.clone(); let mut max_size = 0; - let network = graph.as_network(); + + // A set of saturated variables. We can only remove a variable from here if it's regulator has been changed. let mut saturated = HashSet::new(); 'reach: loop { - for var in network.variables().rev() { + for var in graph.variables().rev() { let next_step = step(graph, &result, var); if next_step.is_empty() { saturated.insert(var); @@ -128,7 +145,7 @@ impl Reachability { println!( " >> [{}/{} saturated] Reach progress: {}[nodes:{}] candidates ({:.2} log-%).", saturated.len(), - network.num_vars(), + graph.num_vars(), result.approx_cardinality(), result.symbolic_size(), (current.log2() / max.log2()) * 100.0 @@ -136,8 +153,8 @@ impl Reachability { } if !saturated.contains(&var) { - for t in network.targets(var) { - saturated.remove(&t); + for t in &targets_of_var[&var] { + saturated.remove(t); } continue 'reach; } From cb535a9b3dc765d174b8cb5896042d610f8911fa Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Tue, 19 Dec 2023 11:29:45 +0100 Subject: [PATCH 3/5] Nicer documentation. --- src/symbolic_async_graph/reachability.rs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/symbolic_async_graph/reachability.rs b/src/symbolic_async_graph/reachability.rs index 4bf57aa..0be6a90 100644 --- a/src/symbolic_async_graph/reachability.rs +++ b/src/symbolic_async_graph/reachability.rs @@ -9,6 +9,7 @@ pub struct Reachability { } impl Reachability { + /// A FWD reachability procedure that uses "structural saturation". pub fn reach_fwd( graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices, @@ -16,6 +17,7 @@ impl Reachability { Self::reach(graph, initial, |g, s, v| g.var_post_out(v, s)) } + /// A BWD reachability procedure that uses "structural saturation". pub fn reach_bwd( graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices, @@ -23,6 +25,7 @@ impl Reachability { Self::reach(graph, initial, |g, s, v| g.var_pre_out(v, s)) } + /// "Basic" saturation FWD reachability procedure. pub fn reach_fwd_basic( graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices, @@ -30,6 +33,7 @@ impl Reachability { Self::reach_basic_saturation(graph, initial, |g, s, v| g.var_post_out(v, s)) } + /// "Basic" saturation BWD reachability procedure. pub fn reach_bwd_basic( graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices, @@ -37,6 +41,7 @@ impl Reachability { Self::reach_basic_saturation(graph, initial, |g, s, v| g.var_pre_out(v, s)) } + /// A basic saturation procedure which performs reachability over all transition functions of a graph. pub fn reach_basic_saturation< F: Fn(&SymbolicAsyncGraph, &GraphColoredVertices, VariableId) -> GraphColoredVertices, >( @@ -91,8 +96,11 @@ impl Reachability { } } - /// Use [`SymbolicAsyncGraph::restrict`] to limit the reachability search to a particular - /// subgraph. + /// A "structural" reachability procedure which uses the dependencies between the update functions to reduce + /// the number of transitions that need to be tested. + /// + /// This sometimes increases the size of the BDDs a little bit, but is overall beneficial in the vast majority + /// of cases. pub fn reach< F: Fn(&SymbolicAsyncGraph, &GraphColoredVertices, VariableId) -> GraphColoredVertices, >( @@ -163,7 +171,7 @@ impl Reachability { if cfg!(feature = "print-progress") { println!( - "Basic reachability done: {}[nodes:{}] candidates. Max intermediate size: {}.", + "Structural reachability done: {}[nodes:{}] candidates. Max intermediate size: {}.", result.approx_cardinality(), result.symbolic_size(), max_size From 34b8c5245febb12717924ce3965d704c156dc074 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Tue, 19 Dec 2023 11:31:39 +0100 Subject: [PATCH 4/5] Remove old reachability methods. --- .../_impl_symbolic_async_graph_algorithm.rs | 27 +++---------------- 1 file changed, 3 insertions(+), 24 deletions(-) diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs index 33825fe..29cdb0b 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs +++ b/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 From 27c34420fd95780247d08baf55ee4d7cfe0b626d Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Tue, 19 Dec 2023 11:57:46 +0100 Subject: [PATCH 5/5] Better reachability test. --- .../_impl_symbolic_async_graph_algorithm.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs index 29cdb0b..8c010fb 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs +++ b/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs @@ -118,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}; @@ -144,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. @@ -158,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]