Add basic percolation method.

src/_impl_space.rs

@@ -1,5 +1,7 @@
+use crate::symbolic_async_graph::SymbolicContext;
 use crate::ExtendedBoolean::{Any, One, Zero};
 use crate::{BooleanNetwork, ExtendedBoolean, Space, VariableId};
+use biodivine_lib_bdd::BddVariable;
 use std::cmp::Ordering;
 use std::fmt::{Display, Formatter};
 use std::ops::{Index, IndexMut};
@@ -75,7 +77,18 @@ impl Space {
         let mut result = Vec::new();
         for (k, v) in self.0.iter().enumerate() {
             if let Some(v) = v.try_as_bool() {
-                result.push((VariableId::from_index(k), v))
+                result.push((VariableId::from_index(k), v));
+            }
+        }
+        result
+    }
+
+    /// The same as [Self::to_values], but uses [BddVariable] instead of [VariableId]. Internal for now.
+    pub(crate) fn to_symbolic_values(&self, context: &SymbolicContext) -> Vec<(BddVariable, bool)> {
+        let mut result = Vec::new();
+        for (k, v) in self.0.iter().enumerate() {
+            if let Some(v) = v.try_as_bool() {
+                result.push((context.state_variables()[k], v));
             }
         }
         result

src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs

@@ -1,5 +1,6 @@
 use crate::biodivine_std::traits::Set;
 use crate::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
+use crate::{ExtendedBoolean, Space, VariableId};
 
 /// Here, we provide several basic symbolic algorithms for exploring the `SymbolicAsyncGraph`.
 /// This mainly includes reachability and similar fixed-point properties.
@@ -81,13 +82,67 @@ impl SymbolicAsyncGraph {
             return result;
         }
     }
+
+    /// Returns `true` if the update function of [VariableId] can evaluate to `false` in the given space.
+    pub fn space_has_var_false(&self, var: VariableId, space: &Space) -> bool {
+        let space = space.to_symbolic_values(self.symbolic_context());
+        !self.get_symbolic_fn_update(var).restrict(&space).is_true()
+    }
+
+    /// Returns `true` if the update function of [VariableId] can evaluate to `true` in the given space.
+    pub fn space_has_var_true(&self, var: VariableId, space: &Space) -> bool {
+        let space = space.to_symbolic_values(self.symbolic_context());
+        !self.get_symbolic_fn_update(var).restrict(&space).is_false()
+    }
+
+    /// Compute a percolation of the given space.
+    ///
+    /// The method has two modes: If `fix_subspace` is set to `true`, the method will only try to update
+    /// variables that are not fixed yet. If `fix_subspace` is `false`, the method can also update variables
+    /// that are fixed in the original space.
+    ///
+    /// If the input is a trap space, these two modes should give the same result.
+    pub fn percolate_space(&self, space: &Space, fix_subspace: bool) -> Space {
+        let mut result = space.clone();
+        'percolate: loop {
+            let symbolic_space = result.to_symbolic_values(self.symbolic_context());
+            for var in self.variables().rev() {
+                if fix_subspace && space[var].is_fixed() {
+                    // In fixed mode, we do not propagate values that are fixed in the original space.
+                    continue;
+                }
+
+                let update = self.get_symbolic_fn_update(var);
+                let restricted = update.restrict(&symbolic_space);
+                let new_value = if restricted.is_true() {
+                    ExtendedBoolean::One
+                } else if restricted.is_false() {
+                    ExtendedBoolean::Zero
+                } else {
+                    ExtendedBoolean::Any
+                };
+
+                if result[var] != new_value {
+                    // If we can update result, we do it and restart the percolation process.
+                    result[var] = new_value;
+                    continue 'percolate;
+                }
+            }
+            // If nothing changed, we are done.
+            break;
+        }
+
+        result
+    }
 }
 
 #[cfg(test)]
 mod tests {
     use crate::biodivine_std::traits::Set;
     use crate::symbolic_async_graph::SymbolicAsyncGraph;
-    use crate::BooleanNetwork;
+    use crate::ExtendedBoolean::Zero;
+    use crate::{BooleanNetwork, ExtendedBoolean, Space};
+    use ExtendedBoolean::One;
 
     #[test]
     pub fn basic_algorithms_test() {
@@ -125,4 +180,57 @@ mod tests {
         // where this is not empty -- less than in the pivot in fact.
         assert!(!repeller_basin.is_empty());
     }
+
+    #[test]
+    fn basic_percolation_test() {
+        let bn = BooleanNetwork::try_from_bnet(
+            r"
+            targets,factors
+            a, a | b
+            b, c & a
+            c, (a & b) | (a & c)
+            ",
+        )
+        .unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
+
+        let a = bn.as_graph().find_variable("a").unwrap();
+        let b = bn.as_graph().find_variable("b").unwrap();
+        let c = bn.as_graph().find_variable("c").unwrap();
+
+        let mut a_true = Space::new(&bn);
+        a_true[a] = One;
+
+        let mut a_false = Space::new(&bn);
+        a_false[a] = Zero;
+
+        let a_true_percolated = stg.percolate_space(&a_true, false);
+        assert_eq!(a_true, a_true_percolated);
+
+        let a_false_percolated = stg.percolate_space(&a_false, false);
+        let mut expected = Space::new(&bn);
+        expected[a] = Zero;
+        expected[b] = Zero;
+        expected[c] = Zero;
+        assert_eq!(expected, a_false_percolated);
+
+        let mut unstable = Space::new(&bn);
+        unstable[b] = One;
+        let mut expected = Space::new(&bn);
+        assert_eq!(expected, stg.percolate_space(&unstable, false));
+        expected[b] = One;
+        expected[a] = One;
+        expected[c] = One;
+        assert_eq!(expected, stg.percolate_space(&unstable, true));
+
+        assert!(stg.space_has_var_false(b, &a_true));
+        assert!(stg.space_has_var_true(b, &a_true));
+        assert!(stg.space_has_var_false(c, &a_true));
+        assert!(stg.space_has_var_true(c, &a_true));
+
+        assert!(stg.space_has_var_false(b, &a_false));
+        assert!(!stg.space_has_var_true(b, &a_false));
+        assert!(stg.space_has_var_false(c, &a_false));
+        assert!(!stg.space_has_var_true(c, &a_false));
+    }
 }