Skip to content

Commit

Permalink
Remove old reachability methods.
Browse files Browse the repository at this point in the history
  • Loading branch information
daemontus committed Dec 19, 2023
1 parent cb535a9 commit 34b8c52
Showing 1 changed file with 3 additions and 24 deletions.
27 changes: 3 additions & 24 deletions src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs
Original file line number Diff line number Diff line change
@@ -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};

Expand All @@ -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
Expand Down

0 comments on commit 34b8c52

Please sign in to comment.